Quelle  Labels.thy

section ‹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₁ l c ==> labels (c₁;;c₂) l (c;;c₂)"

| Labels_Seq2: 
  "labels c₂ l c ==> labels (c₁;;c₂) (l + #:c₁) c"

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

| Labels_CondFalse:
  "labels c₂ l c ==> labels (if (b) c₁ else c₂) (l + #:c₁ + 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"

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₁ c₂)
  note IH1 = ‹∧l c'. labels c₁ l c' ==> l < #:c₁›
  note IH2 = ‹∧l c'. labels c₂ l c' ==> l < #:c₂›
  from ‹labels (c₁;;c₂) l c'› IH1 IH2 show ?case
    by simp(erule labels.cases,auto,force)
next
  case (Cond b c₁ c₂)
  note IH1 = ‹∧l c'. labels c₁ l c' ==> l < #:c₁›
  note IH2 = ‹∧l c'. labels c₂ l c' ==> l < #:c₂›
  from ‹labels (if (b) c₁ else c₂) 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+)
qed


declare One_nat_def [simp del]

lemma less_num_inner_nodes_label:
  "l < #:c ==> ∃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₁ c₂)
  note IH1 = ‹∧l. l < #:c₁ ==> ∃c'. labels c₁ l c'›
  note IH2 = ‹∧l. l < #:c₂ ==> ∃c'. labels c₂ l c'›
  show ?case
  proof(cases "l < #:c₁")
    case True
    from IH1[OF this] obtain c' where "labels c₁ l c'" by auto
    hence "labels (c₁;;c₂) l (c';;c₂)" by(fastforce intro:Labels_Seq1)
    thus ?thesis by auto
  next
    case False
    hence "#:c₁ ≤ l" by simp
    then obtain l' where "l = l' + #:c₁" and "l' = l - #:c₁" by simp
    from ‹l = l' + #:c₁› ‹l < #:c₁;;c₂› have "l' < #:c₂" by simp
    from IH2[OF this] obtain c' where "labels c₂ l' c'" by auto
    with ‹l = l' + #:c₁› have "labels (c₁;;c₂) l c'" by(fastforce intro:Labels_Seq2)
    thus ?thesis by auto
  qed
next
  case (Cond b c₁ c₂)
  note IH1 = ‹∧l. l < #:c₁ ==> ∃c'. labels c₁ l c'›
  note IH2 = ‹∧l. l < #:c₂ ==> ∃c'. labels c₂ 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₁")
      case True
      from IH1[OF this] obtain c' where "labels c₁ l' c'" by auto
      with ‹l = l' + 1› have "labels (if (b) c₁ else c₂) l c'"
        by(fastforce dest:Labels_CondTrue)
      thus ?thesis by auto
    next
      case False
      hence "#:c₁ ≤ l'" by simp
      then obtain l'' where "l' = l'' + #:c₁" and "l'' = l' - #:c₁" by simp
      from ‹l' = l'' + #:c₁› ‹l = l' + 1› ‹l < #:if (b) c₁ else c₂›
      have "l'' < #:c₂" by simp
      from IH2[OF this] obtain c' where "labels c₂ l'' c'" by auto
      with ‹l' = l'' + #:c₁› ‹l = l' + 1› have "labels (if (b) c₁ else c₂) 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
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₁ l c c₂)
  note IH = ‹∧c''. labels c₁ l c'' ==> c = c''›
  from ‹labels c₁ l c› have "l < #:c₁" by(fastforce intro:label_less_num_inner_nodes)
  with ‹labels (c₁;;c₂) l c''› obtain cx where "c'' = cx;;c₂ ∧ labels c₁ l cx"
    by(fastforce elim:labels.cases intro:Labels_Base)
  hence [simp]:"c'' = cx;;c₂" and "labels c₁ l cx" by simp_all
  from IH[OF ‹labels c₁ l cx›] show ?case by simp
next
  case (Labels_Seq2 c₂ l c c₁)
  note IH = ‹∧c''. labels c₂ l c'' ==> c = c''›
  from ‹labels (c₁;;c₂) (l + #:c₁) c''› ‹labels c₂ l c› have "labels c₂ l c''" 
    by(auto elim:labels.cases dest:label_less_num_inner_nodes)
  from IH[OF this] show ?case .
next
  case (Labels_CondTrue c₁ l c b c₂)
  note IH = ‹∧c''. labels c₁ l c'' ==> c = c''›
  from ‹labels (if (b) c₁ else c₂) (l + 1) c''› ‹labels c₁ l c› have "labels c₁ l c''"
    by(fastforce elim:labels.cases dest:label_less_num_inner_nodes)
  from IH[OF this] show ?case .
next
  case (Labels_CondFalse c₂ l c b c₁)
  note IH = ‹∧c''. labels c₂ l c'' ==> c = c''›
  from ‹labels (if (b) c₁ else c₂) (l + #:c₁ + 1) c''› ‹labels c₂ l c›
  have "labels c₂ 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)+


end