Theory Labels

header {* \isaheader{Labels} *}


theory Labels imports Com begin

text {* Labels describe a mapping from the inner node label 
  to the matching command *}

inductive labels :: "cmd => nat => cmd => bool"
where

Labels_Base:
  "labels c 0 c"

| Labels_LAss:
  "labels (V:=e) 1 Skip"

| Labels_Seq1: 
  "labels c⇣1 l c ==> labels (c⇣1;;c⇣2) l (c;;c⇣2)"

| Labels_Seq2: 
  "labels c⇣2 l c ==> labels (c⇣1;;c⇣2) (l + #:c⇣1) c"

| Labels_CondTrue:
  "labels c⇣1 l c ==> labels (if (b) c⇣1 else c⇣2) (l + 1) c"

| Labels_CondFalse:
  "labels c⇣2 l c ==> labels (if (b) c⇣1 else c⇣2) (l + #:c⇣1 + 1) c"

| Labels_WhileBody:
  "labels c' l c ==> labels (while(b) c') (l + 2) (c;;while(b) c')"

| Labels_WhileExit:
  "labels (while(b) c') 1 Skip"

| Labels_Call:
  "labels (Call p es rets) 1 Skip"


lemma label_less_num_inner_nodes:
  "labels c l c' ==> l < #:c"
proof(induct c arbitrary:l c')
  case Skip 
  from `labels Skip l c'` show ?case by(fastforce elim:labels.cases)
next
  case (LAss V e) 
  from `labels (V:=e) l c'` show ?case by(fastforce elim:labels.cases)
next
  case (Seq c⇣1 c⇣2)
  note IH1 = `!!l c'. labels c⇣1 l c' ==> l < #:c⇣1`
  note IH2 = `!!l c'. labels c⇣2 l c' ==> l < #:c⇣2`
  from `labels (c⇣1;;c⇣2) l c'` IH1 IH2 show ?case
    by simp(erule labels.cases,auto,force)
next
  case (Cond b c⇣1 c⇣2)
  note IH1 = `!!l c'. labels c⇣1 l c' ==> l < #:c⇣1`
  note IH2 = `!!l c'. labels c⇣2 l c' ==> l < #:c⇣2`
  from `labels (if (b) c⇣1 else c⇣2) l c'` IH1 IH2 show ?case
    by simp(erule labels.cases,auto,force)
next
  case (While b c)
  note IH = `!!l c'. labels c l c' ==> l < #:c`
  from `labels (while (b) c) l c'` IH show ?case
    by simp(erule labels.cases,fastforce+)
next
  case (Call p es rets) 
  thus ?case by simp(erule labels.cases,fastforce+)
qed


declare One_nat_def [simp del]

lemma less_num_inner_nodes_label:
  assumes "l < #:c" obtains c' where "labels c l c'"
proof(atomize_elim)
  from `l < #:c` show "∃c'. labels c l c'"
  proof(induct c arbitrary:l)
    case Skip
    from `l < #:Skip` have "l = 0" by simp
    thus ?case by(fastforce intro:Labels_Base)
  next
    case (LAss V e)
    from `l < #:(V:=e)` have "l = 0 ∨ l = 1" by auto
    thus ?case by(auto intro:Labels_Base Labels_LAss)
  next
    case (Seq c⇣1 c⇣2)
    note IH1 = `!!l. l < #:c⇣1 ==> ∃c'. labels c⇣1 l c'`
    note IH2 = `!!l. l < #:c⇣2 ==> ∃c'. labels c⇣2 l c'`
    show ?case
    proof(cases "l < #:c⇣1")
      case True
      from IH1[OF this] obtain c' where "labels c⇣1 l c'" by auto
      hence "labels (c⇣1;;c⇣2) l (c';;c⇣2)" by(fastforce intro:Labels_Seq1)
      thus ?thesis by auto
    next
      case False
      hence "#:c⇣1 ≤ l" by simp
      then obtain l' where "l = l' + #:c⇣1" and "l' = l - #:c⇣1" by simp
      from `l = l' + #:c⇣1` `l < #:c⇣1;;c⇣2` have "l' < #:c⇣2" by simp
      from IH2[OF this] obtain c' where "labels c⇣2 l' c'" by auto
      with `l = l' + #:c⇣1` have "labels (c⇣1;;c⇣2) l c'" 
        by(fastforce intro:Labels_Seq2)
      thus ?thesis by auto
    qed
  next
    case (Cond b c⇣1 c⇣2)
    note IH1 = `!!l. l < #:c⇣1 ==> ∃c'. labels c⇣1 l c'`
    note IH2 = `!!l. l < #:c⇣2 ==> ∃c'. labels c⇣2 l c'`
    show ?case
    proof(cases "l = 0")
      case True
      thus ?thesis by(fastforce intro:Labels_Base)
    next
      case False
      hence "0 < l" by simp
      then obtain l' where "l = l' + 1" and "l' = l - 1" by simp
      thus ?thesis
      proof(cases "l' < #:c⇣1")
        case True
        from IH1[OF this] obtain c' where "labels c⇣1 l' c'" by auto
        with `l = l' + 1` have "labels (if (b) c⇣1 else c⇣2) l c'"
          by(fastforce dest:Labels_CondTrue)
        thus ?thesis by auto
      next
        case False
        hence "#:c⇣1 ≤ l'" by simp
        then obtain l'' where "l' = l'' + #:c⇣1" and "l'' = l' - #:c⇣1" by simp
        from `l' = l'' + #:c⇣1` `l = l' + 1` `l < #:if (b) c⇣1 else c⇣2`
        have "l'' < #:c⇣2" by simp
        from IH2[OF this] obtain c' where "labels c⇣2 l'' c'" by auto
        with `l' = l'' + #:c⇣1` `l = l' + 1` have "labels (if (b) c⇣1 else c⇣2) l c'"
          by(fastforce dest:Labels_CondFalse)
        thus ?thesis by auto
      qed
    qed
  next
    case (While b c')
    note IH = `!!l. l < #:c' ==> ∃c''. labels c' l c''`
    show ?case
    proof(cases "l < 1")
      case True
      hence "l = 0" by simp
      thus ?thesis by(fastforce intro:Labels_Base)
    next
      case False
      show ?thesis
      proof(cases "l < 2")
        case True
        with `¬ l < 1` have "l = 1" by simp
        thus ?thesis by(fastforce intro:Labels_WhileExit)
      next
        case False
        with `¬ l < 1` have "2 ≤ l" by simp
        then obtain l' where "l = l' + 2" and "l' = l - 2" 
          by(simp del:add_2_eq_Suc')
        from `l = l' + 2` `l < #:while (b) c'` have "l' < #:c'" by simp
        from IH[OF this] obtain c'' where "labels c' l' c''" by auto
        with `l = l' + 2` have "labels (while (b) c') l (c'';;while (b) c')"
          by(fastforce dest:Labels_WhileBody)
        thus ?thesis by auto
      qed
    qed
  next
    case (Call p es rets)
    show ?case
    proof(cases "l < 1")
      case True
      hence "l = 0" by simp
      thus ?thesis by(fastforce intro:Labels_Base)
    next
      case False
      with `l < #:Call p es rets` have "l = 1" by simp
      thus ?thesis by(fastforce intro:Labels_Call)
    qed
  qed
qed


lemma labels_det:
  "labels c l c'==> (!!c''. labels c l c''==> c' = c'')"
proof(induct rule:labels.induct)
  case (Labels_Base c c'') 
  from `labels c 0 c''` obtain l where "labels c l c''" and "l = 0" by auto
  thus ?case by(induct rule:labels.induct,auto)
next
  case (Labels_Seq1 c⇣1 l c c⇣2)
  note IH = `!!c''. labels c⇣1 l c'' ==> c = c''`
  from `labels c⇣1 l c` have "l < #:c⇣1" by(fastforce intro:label_less_num_inner_nodes)
  with `labels (c⇣1;;c⇣2) l c''` obtain cx where "c'' = cx;;c⇣2 ∧ labels c⇣1 l cx"
    by(fastforce elim:labels.cases intro:Labels_Base)
  hence [simp]:"c'' = cx;;c⇣2" and "labels c⇣1 l cx" by simp_all
  from IH[OF `labels c⇣1 l cx`] show ?case by simp
next
  case (Labels_Seq2 c⇣2 l c c⇣1)
  note IH = `!!c''. labels c⇣2 l c'' ==> c = c''`
  from `labels (c⇣1;;c⇣2) (l + #:c⇣1) c''` `labels c⇣2 l c` have "labels c⇣2 l c''" 
    by(auto elim:labels.cases dest:label_less_num_inner_nodes)
  from IH[OF this] show ?case .
next
  case (Labels_CondTrue c⇣1 l c b c⇣2)
  note IH = `!!c''. labels c⇣1 l c'' ==>  c = c''`
  from `labels (if (b) c⇣1 else c⇣2) (l + 1) c''` `labels c⇣1 l c` have "labels c⇣1 l c''"
    by(fastforce elim:labels.cases dest:label_less_num_inner_nodes)
  from IH[OF this] show ?case .
next
  case (Labels_CondFalse c⇣2 l c b c⇣1)
  note IH = `!!c''. labels c⇣2 l c'' ==>  c = c''`
  from `labels (if (b) c⇣1 else c⇣2) (l + #:c⇣1 + 1) c''` `labels c⇣2 l c`
  have "labels c⇣2 l c''"
    by(fastforce elim:labels.cases dest:label_less_num_inner_nodes)
  from IH[OF this] show ?case .
next
  case (Labels_WhileBody c' l c b)
  note IH = `!!c''. labels c' l c'' ==> c = c''`
  from `labels (while (b) c') (l + 2) c''` `labels c' l c` 
  obtain cx where "c'' = cx;;while (b) c' ∧ labels c' l cx" 
    by -(erule labels.cases,auto)
  hence [simp]:"c'' = cx;;while (b) c'" and "labels c' l cx" by simp_all
  from IH[OF `labels c' l cx`] show ?case by simp
qed (fastforce elim:labels.cases)+



definition label :: "cmd => nat => cmd"
  where "label c n ≡ (THE c'. labels c n c')"


lemma labels_THE:
  "labels c l c' ==> (THE c'. labels c l c') = c'"
by(fastforce intro:the_equality dest:labels_det)


lemma labels_label:"labels c l c' ==> label c l = c'"
by(fastforce intro:labels_THE simp:label_def)


end