text:
           (*-------------------------------------------*
            |  The Dining Mathematicians in CSP-Prover  |
            |               August 2004                 |
            |             December 2004 (modified)      |
            |             November 2005 (modified)      |
            |                March 2007 (modified)      |
            |                 July 2009 (modified)      |
            |        Yoshinao Isobe (AIST JAPAN)        |
            *-------------------------------------------*)

theory DM5_Spc_Imp
imports DM4_Spc_def
begin

(*****************************************************************

         1. proves lemma for Spc <=F Imp
         2.
         3.
         4.

 *****************************************************************)

(*** Back0_Back1 ***)

lemma Back0_Back1:
  "(Spcfun TH0_TH1)<<Spc_to_Imp <=F
   (Back0 -> ($TH0) |[CH0]| ($(VAR x)) |[CH1]| Back1 -> ($TH1))
   -- (CH0 Un CH1)"
apply (cspF_simp unfold_Imp_rules)
apply (cspF_step)+
apply (auto intro!: cspF_decompo_subset)
apply (cspF_simp)+
apply (rule cspF_Int_choice_left1)
apply (rule cspF_Int_choice_left1)
apply (rule cspF_Int_choice_left1)
apply (rule cspF_Int_choice_left1)
apply (rule cspF_Int_choice_left1)
apply (rule cspF_Int_choice_left1)
apply (rule cspF_Int_choice_left1)
apply (rule cspF_Int_choice_left1)
apply (rule cspF_Int_choice_left1)
apply (rule cspF_Int_choice_left1)
apply (rule cspF_Int_choice_left2)
apply (rule cspF_Rep_int_choice_left)
apply (simp)
apply (rule_tac x="x" in exI)
apply (simp)

apply (cspF_simp)+
apply (rule cspF_Int_choice_left1)
apply (rule cspF_Int_choice_left1)
apply (rule cspF_Int_choice_left1)
apply (rule cspF_Int_choice_left1)
apply (rule cspF_Int_choice_left1)
apply (rule cspF_Int_choice_left1)
apply (rule cspF_Int_choice_left1)
apply (rule cspF_Int_choice_left1)
apply (rule cspF_Int_choice_left1)
apply (rule cspF_Int_choice_left2)
apply (rule cspF_Rep_int_choice_left)
apply (simp)
apply (rule_tac x="x" in exI)
apply (simp)
done

lemmas Back0_Back1_simp[simp] = Back0_Back1[simplified]

(*** Eat0_Back1 ***)

lemma Eat0_Back1:
  "~ ODD x ==>
   (Spcfun TH0_TH1)<<Spc_to_Imp <=F
   (Eat0 -> ($(EAT0 x)) |[CH0]| ($(VAR x)) |[CH1]| Back1 -> ($TH1))
      -- (CH0 Un CH1)"
apply (cspF_simp unfold_Imp_rules)
apply (cspF_step)+
apply (auto intro!: cspF_decompo_subset)
apply (cspF_simp)+
apply (rule cspF_Int_choice_left1)
apply (rule cspF_Int_choice_left1)
apply (rule cspF_Int_choice_left1)
apply (rule cspF_Int_choice_left1)
apply (rule cspF_Int_choice_left1)
apply (rule cspF_Int_choice_left2)
apply (rule cspF_Rep_int_choice_left)
apply (simp)
apply (rule_tac x="x" in exI)
apply (simp)

apply (cspF_simp)+
apply (rule cspF_Int_choice_left2)
apply (rule cspF_Rep_int_choice_left)
apply (simp)
apply (rule_tac x="x" in exI)
apply (simp)
done

lemmas Eat0_Back1_simp[simp] = Eat0_Back1[simplified]

(*** Back0_Eat1 ***)

lemma Back0_Eat1:
  "ODD x
   ==>
   (Spcfun TH0_TH1)<<Spc_to_Imp <=F
   (Back0 -> ($TH0) |[CH0]| ($(VAR x)) |[CH1]| Eat1 -> ($(EAT1 x)))
      -- (CH0 Un CH1)"
apply (cspF_simp unfold_Imp_rules)
apply (cspF_step)+
apply (auto intro!: cspF_decompo_subset)
apply (cspF_simp)+
apply (rule cspF_Int_choice_left1)
apply (rule cspF_Int_choice_left1)
apply (rule cspF_Int_choice_left1)
apply (rule cspF_Int_choice_left1)
apply (rule cspF_Int_choice_left2)
apply (rule cspF_Rep_int_choice_left)
apply (simp)
apply (rule_tac x="x" in exI)
apply (simp)

apply (cspF_simp)+
apply (rule cspF_Int_choice_left2)
apply (rule cspF_Rep_int_choice_left)
apply (simp)
apply (rule_tac x="x" in exI)
apply (simp)
done

lemmas Back0_Eat1_simp[simp] = Back0_Eat1[simplified]

lemma EAT0_Back1:
  "~ ODD x
   ==>
   (Spcfun EAT0_TH1)<<Spc_to_Imp <=F
   (($(EAT0 x)) |[CH0]| ($(VAR x))
                      |[CH1]| Back1 -> ($TH1)) -- (CH0 Un CH1)"
apply (cspF_simp unfold_Imp_rules)
apply (cspF_step)+
apply (auto intro!: cspF_decompo_subset)
apply (cspF_simp)+
apply (rule cspF_Int_choice_left1)
apply (rule cspF_Rep_int_choice_left)
apply (simp)
apply (rule_tac x="x" in exI)
apply (simp)

apply (cspF_simp)+
apply (rule cspF_Int_choice_left1)
apply (rule cspF_Int_choice_left1)
apply (rule cspF_Int_choice_left2)
apply (rule cspF_Rep_int_choice_left)
apply (simp)
apply (rule_tac x="x" in exI)
apply (simp)
done

lemmas EAT0_Back1_simp[simp] = EAT0_Back1[simplified]

(*** Back0_EAT1 ***)

lemma Back0_EAT1:
  "ODD x
   ==>
    (Spcfun TH0_EAT1)<<Spc_to_Imp <=F
   (Back0 -> ($TH0) |[CH0]| ($(VAR x)) |[CH1]| ($(EAT1 x)))
    -- (CH0 Un CH1)"
apply (cspF_simp unfold_Imp_rules)
apply (cspF_step)+
apply (auto intro!: cspF_decompo_subset)
apply (cspF_simp)+
apply (rule cspF_Int_choice_left1)
apply (rule cspF_Rep_int_choice_left)
apply (simp)
apply (rule_tac x="x" in exI)
apply (simp)

apply (cspF_simp)+
apply (rule cspF_Int_choice_left2)
apply (rule cspF_Rep_int_choice_left)
apply (simp)
apply (rule_tac x="x" in exI)
apply (simp)
done

lemmas Back0_EAT1_simp[simp] = Back0_EAT1[simplified]

(*** Back0_TH1  ***)

(* declare SpcDef.simps [simp del] *)

lemma Back0_TH1:
  "(Spcfun TH0_TH1)<<Spc_to_Imp <=F
  (Back0 -> ($TH0) |[CH0]| ($(VAR x)) |[CH1]| ($TH1)) -- (CH0 Un CH1)"
apply (cspF_simp unfold_Imp_rules)
apply (rule cspF_Timeout_right)
apply (cspF_step)
apply (auto intro!: cspF_decompo_subset)
apply (cspF_simp)+
apply (rule cspF_Int_choice_left1)+
apply (rule cspF_Rep_int_choice_left)
apply (simp)
apply (rule_tac x="x" in exI)
apply (simp)

apply (case_tac "ODD x")
apply (cspF_simp)+
done

lemmas Back0_TH1_simp[simp] = Back0_TH1[simplified]

(*** TH0_Back1  ***)

lemma TH0_Back1:
  "(Spcfun TH0_TH1)<<Spc_to_Imp <=F
    (($TH0) |[CH0]| ($(VAR x)) |[CH1]| Back1 -> ($TH1)) -- (CH0 Un CH1)"
apply (cspF_simp unfold_Imp_rules)
apply (rule cspF_Timeout_right)
apply (cspF_step)
apply (auto intro!: cspF_decompo_subset)
apply (cspF_simp)+
apply (rule cspF_Int_choice_left1)+
apply (rule cspF_Rep_int_choice_left)
apply (simp)
apply (rule_tac x="x" in exI)
apply (simp)

apply (case_tac "ODD x")
apply (cspF_simp)+
done

lemmas TH0_Back1_simp[simp] = TH0_Back1[simplified]

(*** TH0_Eat1 ***)

lemma TH0_Eat1:
  "ODD x
   ==>
   (Spcfun TH0_TH1)<<Spc_to_Imp <=F
   (($TH0) |[CH0]| ($(VAR x)) |[CH1]| Eat1 -> ($(EAT1 x)))
    -- (CH0 Un CH1)"
apply (cspF_simp unfold_Imp_rules)+
apply (rule cspF_Timeout_right)
apply (cspF_step)
apply (auto intro!: cspF_decompo_subset)
apply (cspF_simp)+
apply (rule cspF_Int_choice_left1)
apply (rule cspF_Rep_int_choice_left)
apply (simp)
apply (rule_tac x="x" in exI)
apply (simp)

apply (cspF_step_right)+
apply (auto intro!: cspF_decompo_subset)
apply (cspF_simp)+
apply (rule cspF_Int_choice_left1)
apply (rule cspF_Int_choice_left1)
apply (rule cspF_Int_choice_left1)
apply (rule cspF_Int_choice_left1)
apply (rule cspF_Int_choice_left2)
apply (rule cspF_Rep_int_choice_left)
apply (simp)
apply (rule_tac x="x" in exI)
apply (simp)

apply (cspF_simp)+
apply (rule cspF_Int_choice_left2)
apply (rule cspF_Rep_int_choice_left)
apply (simp)
apply (rule_tac x="x" in exI)
apply (simp)
done

lemmas TH0_Eat1_simp[simp] = TH0_Eat1[simplified]

(*** Eat0_TH1 ***)

lemma Eat0_TH1:
  "~ ODD x
   ==>
  (Spcfun TH0_TH1)<<Spc_to_Imp <=F
   (Eat0 -> ($(EAT0 x)) |[CH0]| ($(VAR x)) |[CH1]| ($TH1))
    -- (CH0 Un CH1)"
apply (cspF_simp unfold_Imp_rules)+
apply (rule cspF_Timeout_right)
apply (cspF_step)
apply (auto intro!: cspF_decompo_subset)
apply (cspF_simp)+
apply (rule cspF_Int_choice_left1)
apply (rule cspF_Rep_int_choice_left)
apply (simp)
apply (rule_tac x="x" in exI)
apply (simp)

apply (cspF_step_right)+
apply (auto intro!: cspF_decompo_subset)
apply (cspF_simp)+
apply (rule cspF_Int_choice_left1)
apply (rule cspF_Int_choice_left1)
apply (rule cspF_Int_choice_left1)
apply (rule cspF_Int_choice_left1)
apply (rule cspF_Int_choice_left1)
apply (rule cspF_Int_choice_left2)
apply (rule cspF_Rep_int_choice_left)
apply (simp)
apply (rule_tac x="x" in exI)
apply (simp)

apply (cspF_simp)+
apply (rule cspF_Int_choice_left2)
apply (rule cspF_Rep_int_choice_left)
apply (simp)
apply (rule_tac x="x" in exI)
apply (simp)
done

lemmas Eat0_TH1_simp[simp] = Eat0_TH1[simplified]

(*** TH0_TH1 ***)

lemma TH0_TH1:
  "(Spcfun TH0_TH1)<<Spc_to_Imp <=F
    (($TH0) |[CH0]| ($(VAR x)) |[CH1]| ($TH1)) -- (CH0 Un CH1)"
apply (cspF_simp unfold_Imp_rules)
apply (rule)

apply (case_tac "ODD x")
apply (cspF_simp)+

apply (case_tac "ODD x")
apply (cspF_simp)+
done

lemmas TH0_TH1_simp[simp] = TH0_TH1[simplified]

(*** Back0_TH0_TH1 ***)

lemma Back0_TH0_WR1:
  "ODD x
    ==>
        (Spcfun TH0_TH1)<<Spc_to_Imp <=F
        Back0 -> (($TH0) |[CH0]| ($(VAR (3 * x + 1))) |[CH1]| ($TH1))
         -- (CH0 Un CH1)"
apply (cspF_step)
apply (auto intro!: cspF_decompo_subset)
apply (cspF_simp)+
apply (rule cspF_Int_choice_left1)+
apply (rule cspF_Rep_int_choice_left)
apply (simp)
apply (rule_tac x="(3 * x + 1)" in exI)
apply (simp)
done

lemmas Back0_TH0_WR1_simp[simp] = Back0_TH0_WR1[simplified]

(*** Back1_TH0_TH1 ***)

lemma Back1_TH0_WR1:
  "ODD x
    ==>
        (Spcfun TH0_TH1)<<Spc_to_Imp <=F
        Back1 -> (($TH0) |[CH0]| ($(VAR (3 * x + 1))) |[CH1]| ($TH1))
         -- (CH0 Un CH1)"
apply (cspF_step)
apply (auto intro!: cspF_decompo_subset)
apply (cspF_simp)+
apply (rule cspF_Int_choice_left1)+
apply (rule cspF_Rep_int_choice_left)
apply (simp)
apply (rule_tac x="(3 * x + 1)" in exI)
apply (simp)
done

lemmas Back1_TH0_WR1_simp[simp] = Back1_TH0_WR1[simplified]

(*** Back0_WR1 ***)

lemma Back0_WR1:
  "ODD x
   ==>
    (Spcfun TH0_TH1)<<Spc_to_Imp <=F
   (Back0 -> ($TH0) |[CH0]| ($(VAR x))
                          |[CH1]| WR1 (3 * x + 1) -> ($TH1))
   -- (CH0 Un CH1)"
apply (cspF_simp unfold_Imp_rules)
apply (rule cspF_Timeout_right)
apply (cspF_step)
apply (auto intro!: cspF_decompo_subset)
apply (cspF_simp)+
apply (rule cspF_Int_choice_left1)
apply (rule cspF_Int_choice_left2)
apply (rule cspF_Rep_int_choice_left)
apply (simp)
apply (rule_tac x="x" in exI)
apply (simp)
done

lemmas Back0_WR1_simp[simp] = Back0_WR1[simplified]

(*** WR0_Back1 ***)

lemma WR0_Back1:
  "~ ODD x
   ==>
    (Spcfun TH0_TH1)<<Spc_to_Imp <=F
   (WR0 (x div 2) -> ($TH0) |[CH0]| ($(VAR x)) |[CH1]| Back1 -> ($TH1))
       -- (CH0 Un CH1)"
apply (cspF_simp unfold_Imp_rules)
apply (rule cspF_Timeout_right)
apply (cspF_step)
apply (auto intro!: cspF_decompo_subset)
apply (cspF_simp)+
apply (rule cspF_Int_choice_left1)
apply (rule cspF_Int_choice_left1)
apply (rule cspF_Int_choice_left1)
apply (rule cspF_Int_choice_left2)
apply (rule cspF_Rep_int_choice_left)
apply (simp)
apply (rule_tac x="x" in exI)
apply (simp)
done

lemmas WR0_Back1_simp[simp] = WR0_Back1[simplified]

(*** TH0_WR1 ***)

lemma TH0_WR1:
  "ODD x
   ==>
   (Spcfun TH0_TH1)<<Spc_to_Imp <=F
   (($TH0) |[CH0]| ($(VAR x)) |[CH1]| WR1 (3 * x + 1) -> ($TH1))
      -- (CH0 Un CH1)"
apply (cspF_simp unfold_Imp_rules)
apply (rule)
apply (cspF_simp fold_Imp_rules)+
done

lemmas TH0_WR1_simp[simp] = TH0_WR1[simplified]

(*** WR0_TH1 ***)

lemma WR0_TH1:
  "~ ODD x
   ==>
   (Spcfun TH0_TH1)<<Spc_to_Imp <=F
   (WR0 (x div 2) -> ($TH0) |[CH0]| ($(VAR x)) |[CH1]| ($TH1))
     -- (CH0 Un CH1)"
apply (cspF_simp unfold_Imp_rules)
apply (rule)
apply (cspF_simp fold_Imp_rules)
done

lemmas WR0_TH1_simp[simp] = WR0_TH1[simplified]

(*** EAT0_TH1 ***)

lemma EAT0_TH1:
  "~ ODD x
   ==>
   (Spcfun EAT0_TH1)<<Spc_to_Imp <=F
    (($(EAT0 x)) |[CH0]| ($(VAR x)) |[CH1]| ($TH1)) -- (CH0 Un CH1)"
apply (cspF_simp unfold_Imp_rules)
apply (rule cspF_Timeout_right)
apply (cspF_step)
apply (auto intro!: cspF_decompo_subset)
apply (cspF_simp)+
apply (rule cspF_Int_choice_left1)
apply (rule cspF_Int_choice_left1)
apply (rule cspF_Int_choice_left1)
apply (rule cspF_Int_choice_left2)
apply (rule cspF_Rep_int_choice_left)
apply (simp)
apply (rule_tac x="x" in exI)
apply (simp)
done

lemmas EAT0_TH1_simp[simp] = EAT0_TH1[simplified]

(*** TH0_EAT1 ***)

lemma TH0_EAT1:
  "ODD x
   ==>
   (Spcfun TH0_EAT1)<<Spc_to_Imp <=F
    (($TH0) |[CH0]| ($(VAR x)) |[CH1]| ($(EAT1 x))) -- (CH0 Un CH1)"
apply (cspF_simp unfold_Imp_rules)
apply (rule cspF_Timeout_right)
apply (cspF_step)
apply (auto intro!: cspF_decompo_subset)
apply (cspF_simp)+
apply (rule cspF_Int_choice_left1)
apply (rule cspF_Int_choice_left2)
apply (rule cspF_Rep_int_choice_left)
apply (simp)
apply (rule_tac x="x" in exI)
apply (simp)
done

lemmas TH0_EAT1_simp[simp] = TH0_EAT1[simplified]

(*********************************************************
                  ALL n. Spc <=F Imp n
 *********************************************************)

lemma Spc_ref_Seq: "Spc <=F Imp n"
apply (simp add: Spc_def Imp_def)
apply (rule cspF_fp_induct_left[of _ Spc_to_Imp])
apply (simp)+

(*** body ***)
apply (rule cspF_Int_choice_left1)+
apply (rule cspF_Rep_int_choice_left)
apply (simp)
apply (rule_tac x="n" in exI)
apply (simp)

apply (induct_tac p)
apply (auto)
done

end

author: yoshinao-isobe

repo: CSP-Prover


text:
theory Even imports Main begin

(* Two definitions of the notion of evenness, and inductive and a recursive one: *)

inductive ev :: "nat \<Rightarrow> bool" where
  ev0: "ev 0"
| evSS: "ev n \<Longrightarrow> ev (Suc (Suc n))"

fun evn :: "nat \<Rightarrow> bool" where
  "evn 0 = True"
| "evn (Suc 0) = False"
| "evn (Suc (Suc n)) = evn n"

lemma "ev (Suc (Suc (Suc (Suc 0))))"
apply (rule evSS)
apply (rule evSS)
apply (rule ev0)
done

lemma "ev m \<Longrightarrow> evn m"
apply (induction rule: ev.induct)
by auto

lemma "evn n \<Longrightarrow> ev n"
apply (induction rule: evn.induct)
by (simp_all add: ev0 evSS)

declare ev.intros [simp, intro]

end

author: brunoflores

repo: concrete-semantics-book


text:
theory ConcreteSemantics8_1_Stack
  imports Main "~~/src/HOL/IMP/Big_Step" "~~/src/HOL/IMP/Star"
begin

text \<open>

> Working with proofs on the machine language, we will find it convenient for the program counter to admit negative values,
> The effect of this choice is that various decomposition lemmas about machine executions have nicer algebraic properties and fewer preconditions than their nat counterparts

  In the following, we use the length of lists as integers
  instead of natural numbers. Instead of converting \<^typ>\<open>nat\<close>
  to \<^typ>\<open>int\<close> explicitly, we tell Isabelle to coerce \<^typ>\<open>nat\<close>
  automatically when necessary.
\<close>
declare [[coercion_enabled]]
declare [[coercion "int :: nat \<Rightarrow> int"]]

text\<open>
Missing patterns in function definition:
\<And>b. [] !! b = undefined
Found termination order: "(\<lambda>p. length (fst p)) <*mlex*> {}"
\<close>

fun inth :: "'a list \<Rightarrow> int \<Rightarrow> 'a"(infixl "!!" 100) where
"(x # xs) !! i = (if i = 0 then x else xs !! (i - 1))"

text\<open>
Type unification failed: Clash of types "nat" and "int"

Type error in application: incompatible operand type

Operator:  (<) i :: int \<Rightarrow> bool
Operand:   length xs :: nat

This problem is solved by set declare in top of this theory.
\<close>
lemma inth_append[simp]: "0 \<le> i \<Longrightarrow> (xs @ ys) !! i = (if i < size xs then xs !! i else ys !! (i - size xs))"
  apply(induction xs arbitrary: i)
  (* Unfortunately, the following method is not derived only by sledgehammer *)
   apply (auto simp add: algebra_simps)
  done

abbreviation (output)
  "isize xs == int (length xs)"

notation isize ("size")

datatype instr =
  LOADI int | LOAD vname | ADD | STORE vname |
  JMP int | JMPLESS int | JMPGE int

type_synonym stack = "val list"
type_synonym config = "int \<times> state \<times> stack"

abbreviation "hd2 xs \<equiv> hd (tl xs)"
abbreviation "tl2 xs \<equiv> tl (tl xs)"

fun iexec :: "instr \<Rightarrow> config \<Rightarrow> config" where
"iexec instr (i,s,stk) = (case instr of
  LOADI n \<Rightarrow> (i+1, s, n # stk) |
  LOAD x \<Rightarrow> (i +1, s, s x # stk) |
  ADD \<Rightarrow> (i+1, s, (hd2 stk + hd stk) # tl2 stk) |
  STORE x \<Rightarrow> (i + 1, s(x := hd stk), tl stk) |
  JMP n \<Rightarrow> (i + 1 + n, s, stk)|
  JMPLESS n \<Rightarrow> (if hd2 stk < hd stk then i + 1 + n else i + 1, s, tl2 stk)|
  JMPGE n \<Rightarrow>  (if hd stk \<le> hd2 stk then i + 1 + n else i + 1, s, tl2 stk)
)"

definition exec1 :: "instr list \<Rightarrow> config \<Rightarrow> config \<Rightarrow> bool" ("(_/ \<turnstile> (_ \<rightarrow>/ _))" [59,0,59] 60)where
"P \<turnstile> c \<rightarrow> c' =
(\<exists>i s stk. c = (i,s,stk) \<and> c' = iexec(P!!i) (i,s,stk) \<and> 0 \<le> i \<and> i < size P)"

lemma exec1I [intro, code_pred_intro]:
  "c' = iexec (P!!i) (i,s,stk) \<Longrightarrow> 0 \<le> i \<Longrightarrow> i < size P
  \<Longrightarrow> P \<turnstile> (i,s,stk) \<rightarrow> c'"
  by (simp add: exec1_def)

abbreviation exec :: "instr list \<Rightarrow> config \<Rightarrow> config \<Rightarrow> bool" ("(_/ \<turnstile> (_ \<rightarrow>*/ _))" [59,0,59] 60)where
"exec P \<equiv> star (exec1 P)"

lemmas exec_induct = star.induct [of "exec1 P", split_format(complete)]

text\<open>this code_pred are not proved by using `metis` without the above lemma "exec1I"\<close>
code_pred exec1 by (metis exec1_def)

text\<open>
Without `code_pred exec1`, Following values are not calculated by the following reason:
  No mode possible for comprehension
\<close>
values "{(i, map t [''x'', ''y''], stk ) | i t stk. [LOAD ''y'', STORE ''x''] \<turnstile> (0, <''x'' := 3, ''y'' := 4>, []) \<rightarrow>* (i, t, stk )}"

(*lemma 8.4*)
lemma iexec_shift [simp]:
  "((n+i',s',stk') = iexec x (n+i,s,stk)) \<longleftrightarrow> ((i',s',stk') = iexec x (i,s,stk))"
  apply(auto split:instr.split)
  done
text \<open>The split modifier is the hint to auto to perform a case split whenever it sees
a case expression over instr. Thus we guide auto towards the case distinction we made in our proof above.\<close>

lemma exec1_appendR: "P \<turnstile> c \<rightarrow> c' \<Longrightarrow> P@P' \<turnstile> c \<rightarrow> c'"
  apply(auto simp: exec1_def)
  done

(* lemma 8.2 *)
lemma exec_appendR: "P \<turnstile> c \<rightarrow>* c' \<Longrightarrow> P@P' \<turnstile> c \<rightarrow>* c'"
  apply(induction rule: star.induct)
   apply simp
  by (meson exec1_appendR star.step)

lemma exec1_appendL:
  fixes i i' :: int
  shows
  "P \<turnstile> (i,s,stk) \<rightarrow> (i',s',stk') \<Longrightarrow>
   P' @ P \<turnstile> (size(P')+i,s,stk) \<rightarrow> (size(P')+i',s',stk')"
  unfolding exec1_def
  by (auto simp del: iexec.simps)

(* lemma exec1_appendL_other: "P \<turnstile> (i, s, stk) \<rightarrow> (i', s', stk') \<Longrightarrow>
P' @ P \<turnstile> (size P' + i, s, stk) \<rightarrow> (size P' + i', s', stk')"
  apply(auto simp: exec1_def)
  sledgehammer
 *)

(* Lemma 8.3 *)
lemma exec_appendL: "P \<turnstile> (i, s, stk) \<rightarrow>* (i', s', stk') \<Longrightarrow>
P' @ P \<turnstile> (size P' + i, s, stk) \<rightarrow>* (size P' + i', s', stk')"
  apply(induction rule: exec_induct)
   apply simp
  by (meson exec1_appendL star.simps)

(*this lemma is needed to prove the IfFalse part of lemma 8.9*)
lemma exec_Cons_1 [intro]:
  "P \<turnstile> (0,s,stk) \<rightarrow>* (j,t,stk') \<Longrightarrow>
  instr#P \<turnstile> (1,s,stk) \<rightarrow>* (1+j,t,stk')"
by (drule exec_appendL[where P'="[instr]"]) simp

lemma exec_appendL_if[intro]:
  fixes i i' j :: int
  shows
  "size P' <= i
   \<Longrightarrow> P \<turnstile> (i - size P',s,stk) \<rightarrow>* (j,s',stk')
   \<Longrightarrow> i' = size P' + j
   \<Longrightarrow> P' @ P \<turnstile> (i,s,stk) \<rightarrow>* (i',s',stk')"
by (drule exec_appendL[where P'=P']) simp

(* Lemma 8.5 *)
text\<open>The text-book did not write `j''=size P + i'` in the following lemma.
This lack affects the proof of lemma 8.5.
\<close>
lemma exec_append_trans[intro]:"\<lbrakk>
P \<turnstile> (0,s,stk) \<rightarrow>* (i', s', stk');
size P \<le> i';
P' \<turnstile> (i' - size P, s', stk') \<rightarrow>* (i'', s'', stk'');
j'' = size P + i''
\<rbrakk>
 \<Longrightarrow> P @ P' \<turnstile>  (0, s,stk) \<rightarrow>* (j'', s'', stk'')"
  by (meson exec_appendL_if exec_appendR star_trans)

declare Let_def[simp]

subsubsection "8.3 Compilation"

fun acomp :: "aexp \<Rightarrow> instr list" where
"acomp (N n) = [LOADI n]" |
"acomp (V x) = [LOAD x]" |
"acomp (Plus a1 a2) = acomp a1 @ acomp a2 @ [ADD]"

(*Lemma 8.6*)

lemma acomp_correct[intro]:
  "acomp a \<turnstile> (0,s,stk) \<rightarrow>* (size(acomp a),s,aval a s#stk)"
  by (induction a arbitrary: stk) fastforce+

fun bcomp :: "bexp \<Rightarrow> bool \<Rightarrow> int \<Rightarrow> instr list" where
"bcomp (Bc v) f n = (if v=f then [JMP n] else [])" |
"bcomp (Not b) f n = bcomp b (\<not>f) n" |
"bcomp (And b1 b2) f n =
 (let cb2 = bcomp b2 f n;
        m = if f then size cb2 else (size cb2)+n;
      cb1 = bcomp b1 False m
  in cb1 @ cb2)" |
"bcomp (Less a1 a2) f n =
 acomp a1 @ acomp a2 @ (if f then [JMPLESS n] else [JMPGE n])"

value "bcomp (And (Bc True) (Bc True)) False 3"
value "bcomp (And (Bc False) (Bc True)) True 3"
value "bcomp (And (Less (V ''x'') (V ''y'')) (Bc True)) False 3"
value
  "bcomp (And (Less (V ''x'') (V ''y'')) (Not(Less (V ''u'') (V ''v''))))
     False 3"

(* Lemma 8.8 *)
lemma bcomp_correct[intro]:  fixes n :: int
  shows"
0 \<le> n \<Longrightarrow>
bcomp b f n \<turnstile> (0, s, stk) \<rightarrow>* (size(bcomp b f n) + (if f = bval b s then n else 0), s, stk)
"
proof(induction b arbitrary: f n)
  case (Bc x)
  then show ?case by fastforce
next
  case (Not b)
(*  then show ?case
    using bcomp.simps(2) bval.simps(2) by presburger*)
  from Not(1)[where f="~f"] Not(2) show ?case by fastforce
next
  case (And b1 b2)
  from And(1)[of "if f then size(bcomp b2 f n) else size(bcomp b2 f n) + n" "False"]
       And(2)[of n f] And(3)
  show ?case by fastforce
next
  case (Less x1a x2a)
  then show ?case by fastforce
qed

fun ccomp :: "com \<Rightarrow> instr list" where
"ccomp SKIP = []" |
"ccomp (x ::= a) = acomp a @ [STORE x]" |
"ccomp (c\<^sub>1;;c\<^sub>2) = ccomp c\<^sub>1 @ ccomp c\<^sub>2" |
"ccomp (IF b THEN c\<^sub>1 ELSE c\<^sub>2) =
  (let cc\<^sub>1 = ccomp c\<^sub>1; cc\<^sub>2 = ccomp c\<^sub>2; cb = bcomp b False (size cc\<^sub>1 + 1)
   in cb @ cc\<^sub>1 @ JMP (size cc\<^sub>2) # cc\<^sub>2)" |
"ccomp (WHILE b DO c) =
 (let cc = ccomp c; cb = bcomp b False (size cc + 1)
  in cb @ cc @ [JMP (-(size cb + size cc + 1))])"

value "ccomp
 (IF Less (V ''u'') (N 1) THEN ''u'' ::= Plus (V ''u'') (N 1)
  ELSE ''v'' ::= V ''u'')"

value "ccomp (WHILE Less (V ''u'') (N 1) DO (''u'' ::= Plus (V ''u'') (N 1)))"

subsection "8.4 Preservation of Semantics"

(* Lemma 8.9  *)
lemma ccomp_bigstep: "(c,s) \<Rightarrow> t \<Longrightarrow> ccomp c \<turnstile> (0,s,stk) \<rightarrow>* (size (ccomp c), t, stk)"
proof(induction arbitrary: stk rule: big_step_induct)
case (Skip s)
  then show ?case by (fastforce)
next
  case (Assign x a s)
  then show ?case by (fastforce simp:fun_upd_def cong: if_cong)
next
  case (Seq c\<^sub>1 s\<^sub>1 s\<^sub>2 c\<^sub>2 s\<^sub>3)
  let ?cc1 = "ccomp c\<^sub>1" let ?cc2 = "ccomp c\<^sub>2"
  have "?cc1 @ ?cc2 \<turnstile> (0, s\<^sub>1, stk) \<rightarrow>* (size ?cc1, s\<^sub>2, stk)"
    by (simp add: Seq.IH(1) exec_appendR)
  moreover have "?cc1 @ ?cc2 \<turnstile> (size ?cc1, s\<^sub>2, stk) \<rightarrow>* (size (?cc1 @ ?cc2), s\<^sub>3, stk)" using Seq.IH(2) by fastforce
(* ccomp (?c\<^sub>12;; ?c\<^sub>22) \<turnstile> (0, ?s\<^sub>12, ?stka2) \<rightarrow>* (size (ccomp (?c\<^sub>12;; ?c\<^sub>22)), ?s\<^sub>32, ?stka2)  *)
    ultimately show ?case
      by (metis (no_types, lifting) ccomp.simps(3) star_trans)
next
  case (IfTrue b s c\<^sub>1 t c\<^sub>2)
  then show ?case by fastforce
next
  case (IfFalse b s c\<^sub>2 t c\<^sub>1)
  then show ?case by fastforce
next
  case (WhileFalse b s c)
  then show ?case by fastforce
next
  case (WhileTrue b s1 c s2 s3)
  let ?cc = "ccomp c"
  let ?cb = "bcomp b False (size ?cc + 1)"
  let ?cw = "ccomp (WHILE b DO c)"
(*
    bval b s\<^sub>1
    (c, s\<^sub>1) \<Rightarrow> s\<^sub>2
    (WHILE b DO c, s\<^sub>2) \<Rightarrow> s\<^sub>3
    ccomp c \<turnstile> (0, s\<^sub>1, ?stk) \<rightarrow>* (size (ccomp c), s\<^sub>2, ?stk)
    ccomp (WHILE b DO c) \<turnstile> (0, s\<^sub>2, ?stk) \<rightarrow>* (size (ccomp (WHILE b DO c)), s\<^sub>3, ?stk)

goal (1 subgoal):
 1. ccomp (WHILE b DO c) \<turnstile> (0, s\<^sub>1, stk) \<rightarrow>* (size (ccomp (WHILE b DO c)), s\<^sub>3, stk)
*)
  have "?cw \<turnstile> (0,s1,stk) \<rightarrow>* (size ?cb,s1,stk)" using \<open>bval b s1\<close> by fastforce
  have "?cw \<turnstile> (size ?cb,s1,stk) \<rightarrow>* (size ?cb + size ?cc,s2,stk)" using WhileTrue.IH by fastforce
  moreover have "?cw \<turnstile> (size ?cb + size ?cc,s2,stk) \<rightarrow>* (0,s2,stk)" by fastforce
  moreover have "?cw \<turnstile> (0,s2,stk) \<rightarrow>* (size ?cw,s3,stk)"
    using WhileTrue.IH(2) by blast
  ultimately  show ?case
    by (meson \<open>ccomp (WHILE b DO c) \<turnstile> (0, s1, stk) \<rightarrow>* (size (bcomp b False (size (ccomp c) + 1)), s1, stk)\<close> star_trans)
qed

text\<open>the other direction is difficult to solve.\<close>

text \<open>The possible successor PCs of an instruction at position \<^term>\<open>n\<close>\<close>
definition isuccs :: "instr \<Rightarrow> int \<Rightarrow> int set" where
"isuccs i n = (case i of
  JMP j \<Rightarrow> {n + 1 + j} |
  JMPLESS j \<Rightarrow> {n + 1 + j, n + 1} |
  JMPGE j \<Rightarrow> {n + 1 + j, n + 1} |
  _ \<Rightarrow> {n +1})"

text \<open>The possible successors PCs of an instruction list\<close>
definition succs :: "instr list \<Rightarrow> int \<Rightarrow> int set" where
"succs P n = {s. \<exists>i::int. 0 \<le> i \<and> i < size P \<and> s \<in> isuccs (P!!i) (n+i)}"

text \<open>Possible exit PCs of a program\<close>
definition exits :: "instr list \<Rightarrow> int set" where
"exits P = succs P 0 - {0..< size P}"

primrec
  exec_n :: "instr list \<Rightarrow> config \<Rightarrow> nat \<Rightarrow> config \<Rightarrow> bool"
  ("_/ \<turnstile> (_ \<rightarrow>^_/ _)" [65,0,1000,55] 55)
where
  "P \<turnstile> c \<rightarrow>^0 c' = (c'=c)" |
  "P \<turnstile> c \<rightarrow>^(Suc n) c'' = (\<exists>c'. (P \<turnstile> c \<rightarrow> c') \<and> P \<turnstile> c' \<rightarrow>^n c'')"

lemma succs_empty [iff]: "succs [] n = {}"
  by (simp add: succs_def)

lemma succs_Cons:
  "succs (x#xs) n = isuccs x n \<union> succs xs (1+n)" (is "_ = ?x \<union> ?xs")
proof
(*
goal (2 subgoals):
 1. succs (x # xs) n \<subseteq> isuccs x n \<union> succs xs (1 + n)
 2. isuccs x n \<union> succs xs (1 + n) \<subseteq> succs (x # xs) n
*)
  let ?isuccs = "\<lambda>p P n i::int. 0 \<le> i \<and> i < size P \<and> p \<in> isuccs (P!!i) (n+i)"

  have "p \<in> ?x \<union> ?xs" if assm: "p \<in> succs (x#xs) n" for p
  proof -
    (* take i becasuse assumption cotains list*)
    from assm obtain i::int where isuccs: "?isuccs p (x#xs) n i" unfolding succs_def by auto
    show ?thesis
    proof cases
      assume "i = 0"
      with isuccs
      show ?thesis by fastforce
    next
      assume "i \<noteq> 0"
      with isuccs
      have "?isuccs p xs (n+1) (i -1)" by fastforce
      then have "p \<in> ?xs" unfolding succs_def by fastforce
      show ?thesis
        by (simp add: \<open>p \<in> succs xs (1 + n)\<close>)
    qed
  qed
  thus "succs (x#xs) n \<subseteq> ?x \<union> ?xs" ..

  have "p \<in> succs (x#xs) n" if assm: "p \<in> ?x \<or> p \<in> ?xs" for p
  proof -
    from assm show ?thesis
    proof
      assume "p \<in> ?x" thus ?thesis by (auto simp add: succs_def)
    next
      assume "p \<in> ?xs"
      (* in the following where contains (1+n) not (n+1), the latter will fail to prove *)
      then obtain i where "?isuccs p xs (1+n) i" unfolding succs_def by auto
      hence "?isuccs p (x#xs) n (i +1)" by (simp add: algebra_simps)
      thus ?thesis unfolding succs_def
        by blast
    qed
  qed
  thus "?x \<union> ?xs \<subseteq> succs (x#xs) n" by blast
qed

lemma succs_simps [simp]:
  "succs [ADD] n = {n + 1}"
  "succs [LOADI v] n = {n + 1}"
  "succs [LOAD x] n = {n + 1}"
  "succs [STORE x] n = {n + 1}"
  "succs [JMP i] n = {n + 1 + i}"
  "succs [JMPGE i] n = {n + 1 + i, n + 1}"
  "succs [JMPLESS i] n = {n + 1 + i, n + 1}"
  by (auto simp: succs_def isuccs_def)

lemma succs_iexec1:
  assumes "c' = iexec (P!!i) (i,s,stk)" "0 \<le> i" "i < size P"
  shows "fst c' \<in> succs P 0"
  using assms by (auto simp: succs_def isuccs_def split: instr.split)

lemma succs_shift:
  "(p - n \<in> succs P 0) = (p \<in> succs P n)"
  by (fastforce simp: succs_def isuccs_def split: instr.split)

lemma inj_op_plus [simp]:
  "inj ((+) (i::int))"
  by (metis add_minus_cancel inj_on_inverseI)

lemma succs_set_shift [simp]:
  "(+) i ` succs xs 0 = succs xs i"
  by (force simp: succs_shift [where n=i, symmetric] intro: set_eqI)

(* Lemma 8.10 *)
lemma succs_append_otherway [simp]:
  "succs (xs @ ys) n = succs xs n \<union> succs ys (n + size xs)"
proof(induction xs arbitrary:n)
  case Nil
  then show ?case
    by simp
    (*using succs_empty*)
next
  case (Cons a xs)
(* 1. \<And>a xs n. (\<And>n. succs (xs @ ys) n = succs xs n \<union> succs ys (n + size xs)) \<Longrightarrow> succs ((a # xs) @ ys) n = succs (a # xs) n \<union> succs ys (n + size (a # xs))*)
  then show ?case by (auto simp: algebra_simps succs_Cons)
qed

text\<open>the following way what written in Compiler2 is doned with exec_n_exec \<close>
(*
lemma succs_append [simp]:
  "succs (xs @ ys) n = succs xs n \<union> succs ys (n + size xs)"
  apply(induct xs arbitrary: n)
   apply(auto simp: succs_Cons algebra_simps)
  done
*)

(* Lemma 8.11 *)
lemma exec_n_exec:
  "P \<turnstile> c \<rightarrow>^n c' \<Longrightarrow> P \<turnstile> c \<rightarrow>* c'"
  apply(induction n arbitrary: c)
   apply simp
  by (meson exec_n.simps(2) star.step)

lemma exec_exec_n:
  "P \<turnstile> c \<rightarrow>* c' \<Longrightarrow> \<exists>n. P \<turnstile> c \<rightarrow>^n c'"
  apply(induction rule:star.induct)
  using exec_n.simps(1) apply blast
  using exec_n.simps(2) by blast

lemma exec_eq_exec_n:
  "(P \<turnstile> c \<rightarrow>* c') = (\<exists>n. P \<turnstile> c \<rightarrow>^n c')"
  using exec_exec_n exec_n_exec by blast

(* Lemma 8.12. *)

(* To prove the following lemmas, it is needed to show some of the `succs_xxx`.
Especially, proving exits_simps, this needs simplification of succs lemma named `succs_simps`
 *)
lemma exits_append [simp]:
  "exits (xs @ ys) = exits xs \<union> ((+) (size xs)) ` exits ys -
                     {0..<size xs + size ys}"
  by (auto simp: exits_def image_set_diff)

lemma exits_single:
  "exits [x] = isuccs x 0 - {0}"
  by (auto simp: exits_def succs_def)

lemma exits_Cons:
  "exits (x # xs) = (isuccs x 0 - {0}) \<union> ((+) 1) ` exits xs -
                     {0..<1 + size xs}"
  using exits_append [of "[x]" xs]
  by (simp add: exits_single)

lemma exits_empty [iff]: "exits [] = {}" by (simp add: exits_def)

lemma exits_simps [simp]:
  "exits [ADD] = {1}"
  "exits [LOADI v] = {1}"
  "exits [LOAD x] = {1}"
  "exits [STORE x] = {1}"
  "i \<noteq> -1 \<Longrightarrow> exits [JMP i] = {1 + i}"
  "i \<noteq> -1 \<Longrightarrow> exits [JMPGE i] = {1 + i, 1}"
  "i \<noteq> -1 \<Longrightarrow> exits [JMPLESS i] = {1 + i, 1}"
  by (auto simp: exits_def)

lemma acomp_succs [simp]:
  "succs (acomp a) n = {n + 1 .. n + size (acomp a)}"
  apply(induction a arbitrary: n)
    apply(auto simp: exits_def)
  done
(*In the above lemma, `apply(auto simp: exits_def)` needs many subgoals.
So you need prove them as lemma named "exits_simps".
*)

lemma acomp_size:
  "(1::int) \<le> size (acomp a)"
  apply(induction a)
    apply(auto)
  done

lemma acomp_exits [simp]:
  "exits (acomp a) = {size (acomp a)}"
  apply(auto simp: acomp_size exits_def)
  done

(* Lemma 8.13.
we settle for providing an upper bound on the possible successors of bcomp.
*)

lemma bcomp_succs:
  "0 \<le> i \<Longrightarrow>
  succs (bcomp b f i) n \<subseteq> {n .. n + size (bcomp b f i)}
                           \<union> {n + i + size (bcomp b f i)}"
proof(induction b arbitrary: f i n)
  case (Bc x)
  then show ?case by auto
next
  case (Not b)
  then show ?case by auto
next
  case (And b1 b2)
  from And.prems
  show ?case by (cases f) (auto dest: And.IH [THEN subsetD, rotated])
next
  case (Less x1a x2a)
  then show ?case by auto
qed

lemmas bcomp_succsD [dest!] = bcomp_succs [THEN subsetD, rotated]
(* theorem bcomp_succsD:
?c \<in> succs (bcomp ?b ?f ?i) ?n \<Longrightarrow>
0 \<le> ?i \<Longrightarrow>
?c \<in> {?n..?n + size (bcomp ?b ?f ?i)} \<union> {?n + ?i + size (bcomp ?b ?f ?i)} *)

lemma bcomp_exits:
  fixes i :: int
  shows
  "0 \<le> i \<Longrightarrow>
  exits (bcomp b f i) \<subseteq> {size (bcomp b f i), i + size (bcomp b f i)}"
  apply(auto simp:exits_def)
  done

lemma bcomp_exitsD [dest!]:
  "p \<in> exits (bcomp b f i) \<Longrightarrow> 0 \<le> i \<Longrightarrow>
  p = size (bcomp b f i) \<or> p = i + size (bcomp b f i)"
  using bcomp_exits by auto

(* Lemma 8.14. *)

lemma ccomp_succs:
  "succs (ccomp c) n \<subseteq> {n..n + size (ccomp c)}"
proof(induction c arbitrary: n)
  case SKIP
  then show ?case by simp
next
  case (Assign x1 x2)
  then show ?case by simp
next
  case (Seq c1 c2)
  from Seq.prems
  show ?case by (fastforce dest: Seq.IH[THEN subsetD])
next
  case (If x1 c1 c2)
  from If.prems
  show ?case by (auto dest: If.IH[THEN subsetD] simp: isuccs_def succs_Cons)
next
  case (While x1 c)
  from While.prems
  show ?case by (auto dest: While.IH[THEN subsetD])
qed

lemma ccomp_exits:
  "exits (ccomp c) \<subseteq> {size (ccomp c)}"
  using ccomp_succs [of c 0] by (auto simp: exits_def)

(* Lemma 8.15 (Decomposition of machine executions). *)
lemma exec_Suc:
  "\<lbrakk> P \<turnstile> c \<rightarrow> c'; P \<turnstile> c' \<rightarrow>^n c'' \<rbrakk> \<Longrightarrow> P \<turnstile> c \<rightarrow>^(Suc n) c''"
  by (fastforce simp del: split_paired_Ex)

lemma exec_n_Nil [simp]:
  "[] \<turnstile> c \<rightarrow>^k c' = (c' = c \<and> k = 0)"
  by (induct k) (auto simp: exec1_def)

lemma exec1_exec_n [intro!]:
  "P \<turnstile> c \<rightarrow> c' \<Longrightarrow> P \<turnstile> c \<rightarrow>^1 c'"
  by (cases c') simp

lemma exec1_split:
  fixes i j :: int
  shows
  "P @ c @ P' \<turnstile> (size P + i, s) \<rightarrow> (j,s') \<Longrightarrow> 0 \<le> i \<Longrightarrow> i < size c \<Longrightarrow>
  c \<turnstile> (i,s) \<rightarrow> (j - size P, s')"
  apply(auto simp: exec1_def)
  apply(auto split: instr.splits)
  done

lemma exec_n_split:
  fixes i j :: int
  assumes "P @ c @ P' \<turnstile> (size P + i, s) \<rightarrow>^n (j, s')"
          "0 \<le> i" "i < size c"
          "j \<notin> {size P ..< size P + size c}"
  shows "\<exists>s'' (i'::int) k m.
                   c \<turnstile> (i, s) \<rightarrow>^k (i', s'') \<and>
                   i' \<in> exits c \<and>
                   P @ c @ P' \<turnstile> (size P + i', s'') \<rightarrow>^m (j, s') \<and>
                   n = k + m"
using assms proof (induction n arbitrary: i j s)
  case 0
  then show ?case
    by simp
next
  case (Suc n)
  have i: "0 \<le> i" "i < size c" by fact+
  from Suc.prems
  have j: "\<not> (size P \<le> j \<and> j < size P + size c)" by simp
  obtain i0 s0 where
    step: "P @ c @ P' \<turnstile> (size P + i, s) \<rightarrow> (i0,s0)" and
    rest: "P @ c @ P' \<turnstile> (i0,s0) \<rightarrow>^n (j, s')"
    using Suc.prems(1) by auto
  from step i
  have c: "c \<turnstile> (i,s) \<rightarrow> (i0 - size P, s0)" by(rule exec1_split)

  have "i0 = size P + (i0 - size P) " by simp
  then obtain j0::int where j0: "i0 = size P + j0" ..

note split_paired_Ex [simp del]

  have ?case if assm: "j0 \<in> {0 ..< size c}"
  proof -
    from assm j0 j rest c
    show ?case by (fastforce dest!: Suc.IH intro!: exec_Suc)
  qed
  moreover have ?case if assm: "j0 \<notin> {0 ..< size c}"
  proof -
    from c j0 have "j0 \<in> succs c 0"
      by (auto dest: succs_iexec1 simp: exec1_def simp del: iexec.simps)
    with assm have "j0 \<in> exits c" by (simp add: exits_def)
    with c j0 rest show ?case by fastforce
    (* exec1_exec_n is needed to prove over case. *)
(*      by (metis add.commute add.left_neutral add_Suc diff_eq_eq exec_n.simps(1) exec_n.simps(2)) *)
  qed
  ultimately show ?case
    by blast
qed

subsection \<open>Concrete symbolic execution steps\<close>

lemma exec_0 [intro!]: "P \<turnstile> c \<rightarrow>^0 c" by simp

lemma exec_n_step:
  "n \<noteq> n' \<Longrightarrow>
  P \<turnstile> (n,stk,s) \<rightarrow>^k (n',stk',s') =
  (\<exists>c. P \<turnstile> (n,stk,s) \<rightarrow> c \<and> P \<turnstile> c \<rightarrow>^(k - 1) (n',stk',s') \<and> 0 < k)"
  by (cases k) auto

lemma exec1_end:
  "size P <= fst c \<Longrightarrow> \<not> P \<turnstile> c \<rightarrow> c'"
  by (auto simp: exec1_def)

lemma exec_n_end:
  "size P <= (n::int) \<Longrightarrow>
  P \<turnstile> (n,s,stk) \<rightarrow>^k (n',s',stk') = (n' = n \<and> stk'=stk \<and> s'=s \<and> k =0)"
  by (cases k) (auto simp: exec1_end)

lemmas exec_n_simps = exec_n_step exec_n_end

lemma exec1_drop_left:
  fixes i n :: int
  assumes "P1 @ P2 \<turnstile> (i, s, stk) \<rightarrow> (n, s', stk')" and "size P1 \<le> i"
  shows "P2 \<turnstile> (i - size P1, s, stk) \<rightarrow> (n - size P1, s', stk')"
proof -
  have "i = size P1 + (i - size P1)" by simp
  then obtain i' :: int where "i = size P1 + i'" ..
  moreover
  have "n = size P1 + (n - size P1)" by simp
  then obtain n' :: int where "n = size P1 + n'" ..
  ultimately
  show ?thesis using assms
    by (clarsimp simp: exec1_def simp del: iexec.simps)
qed

lemma exec_n_drop_left:
  fixes i n :: int
  assumes "P @ P' \<turnstile> (i, s, stk) \<rightarrow>^k (n, s', stk')"
          "size P \<le> i" "exits P' \<subseteq> {0..}"
  shows "P' \<turnstile> (i - size P, s, stk) \<rightarrow>^k (n - size P, s', stk')"
using assms proof (induction k arbitrary: i s stk)
  case 0 thus ?case by simp
next
  case (Suc k)
  from Suc.prems
  obtain i' s'' stk'' where
    step: "P @ P' \<turnstile> (i, s, stk) \<rightarrow> (i', s'', stk'')" and
    rest: "P @ P' \<turnstile> (i', s'', stk'') \<rightarrow>^k (n, s', stk')"
    by auto
  from step \<open>size P \<le> i\<close>
  have *: "P' \<turnstile> (i - size P, s, stk) \<rightarrow> (i' - size P, s'', stk'')"
    by (rule exec1_drop_left)
  then have "i' - size P \<in> succs P' 0"
    by (fastforce dest!: succs_iexec1 simp: exec1_def simp del: iexec.simps)
  with \<open>exits P' \<subseteq> {0..}\<close>
  have "size P \<le> i'" by (auto simp: exits_def)
  from rest this \<open>exits P' \<subseteq> {0..}\<close>
  have "P' \<turnstile> (i' - size P, s'', stk'') \<rightarrow>^k (n - size P, s', stk')"
    by (rule Suc.IH)
  with * show ?case by auto
qed

lemma exec_n_split_full:
  fixes j :: int
  assumes exec: "P @ P' \<turnstile> (0,s,stk) \<rightarrow>^k (j, s', stk')"
  assumes P: "size P \<le> j"
  assumes closed: " exits P \<subseteq> {size P}"
  assumes exits: "exits P' \<subseteq> {0..}"
  shows "\<exists>k1 k2 s'' stk''. P \<turnstile> (0,s,stk) \<rightarrow>^k1 (size P, s'', stk'') \<and>
                           P' \<turnstile> (0,s'',stk'') \<rightarrow>^k2 (j - size P, s', stk')"
proof (cases "P")
  case Nil
  then show ?thesis
    using exec by auto
next
  case (Cons a list)
  hence "0 < size P" by simp
  with exec P closed
  obtain k1 k2 s'' stk'' where
    1: "P \<turnstile> (0,s,stk) \<rightarrow>^k1 (size P, s'', stk'')" and
    2: "P @ P' \<turnstile> (size P,s'',stk'') \<rightarrow>^k2 (j, s', stk')"
    by (auto dest!: exec_n_split [where P="[]" and i=0, simplified])
  moreover have "j = size P + (j - size P)" by simp
  then obtain j0 :: int where "j = size P + j0" ..
  ultimately show ?thesis using exits by (fastforce dest: exec_n_drop_left)
qed

(* Lemma 8.16 (Correctness of acomp, reverse direction). *)

lemma acomp_exec_n [dest!]:
  "acomp a \<turnstile> (0,s,stk) \<rightarrow>^n (size (acomp a),s',stk') \<Longrightarrow>
  s' = s \<and> stk' = aval a s#stk"
proof(induction a arbitrary: n s' stk stk')
case (N x)
  then show ?case by (auto simp: exec_n_simps exec1_def)
next
case (V x)
  then show ?case  by (auto simp: exec_n_simps exec1_def)
next
  case (Plus a1 a2)
  from Plus.prems
  have "acomp a1 @ acomp a2 @ [ADD] \<turnstile> (0,s,stk) \<rightarrow>^n (size (acomp a1) + (size (acomp a2) + 1), s', stk')"
    by (simp add: algebra_simps)
  then obtain n1 s1 stk1 n2 s2 stk2 n3 where
    "acomp a1 \<turnstile> (0,s,stk) \<rightarrow>^n1 (size (acomp a1), s1, stk1)"
    "acomp a2 \<turnstile> (0,s1,stk1) \<rightarrow>^n2 (size (acomp a2), s2, stk2)"
       "[ADD] \<turnstile> (0,s2,stk2) \<rightarrow>^n3 (1, s', stk')" by (auto dest!: exec_n_split_full)
  then show ?case by (fastforce dest: Plus.IH simp: exec_n_simps exec1_def)
qed

(*Lemma 8.17 (Correctness of bcomp, reverse direction).*)

lemma exec_n_drop_right:
  fixes j :: int
  assumes "c @ P' \<turnstile> (0, s) \<rightarrow>^n (j, s')" "j \<notin> {0..<size c}"
  shows "\<exists>s'' i' k m.
          (if c = [] then s'' = s \<and> i' = 0 \<and> k = 0
           else c \<turnstile> (0, s) \<rightarrow>^k (i', s'') \<and>
           i' \<in> exits c) \<and>
           c @ P' \<turnstile> (i', s'') \<rightarrow>^m (j, s') \<and>
           n = k + m"
  using assms
  by (cases "c = []")
     (auto dest: exec_n_split [where P="[]", simplified])

lemma bcomp_split:
  fixes i j :: int
  assumes "bcomp b f i @ P' \<turnstile> (0, s, stk) \<rightarrow>^n (j, s', stk')"
          "j \<notin> {0..<size (bcomp b f i)}" "0 \<le> i"
  shows "\<exists>s'' stk'' (i'::int) k m.
           bcomp b f i \<turnstile> (0, s, stk) \<rightarrow>^k (i', s'', stk'') \<and>
           (i' = size (bcomp b f i) \<or> i' = i + size (bcomp b f i)) \<and>
           bcomp b f i @ P' \<turnstile> (i', s'', stk'') \<rightarrow>^m (j, s', stk') \<and>
           n = k + m"
  using assms by (cases "bcomp b f i = []") (fastforce dest!: exec_n_drop_right)+

lemma bcomp_exec_n [dest]:
  fixes i j :: int
  assumes "bcomp b f j \<turnstile> (0, s, stk) \<rightarrow>^n (i, s', stk')"
          "size (bcomp b f j) \<le> i" "0 \<le> j"
  shows "i = size(bcomp b f j) + (if f = bval b s then j else 0) \<and>
         s' = s \<and> stk' = stk"
using assms proof (induction b arbitrary: f j i n s' stk')
  case (Bc x)
  then show ?case  by (simp split: if_split_asm add: exec_n_simps exec1_def)
next
  case (Not b)
  from Not.prems show ?case
    by (fastforce dest!: Not.IH)
next
  case (And b1 b2)
  then show ?case sorry
next
  case (Less x1a x2a)
  then show ?case by (auto dest!: exec_n_split_full simp: exec_n_simps exec1_def)
qed

lemma ccomp_exec_n:
  "ccomp c \<turnstile> (0,s,stk) \<rightarrow>^n (size(ccomp c),t,stk')
  \<Longrightarrow> (c,s) \<Rightarrow> t \<and> stk'=stk"
proof (induction c arbitrary: s t stk stk' n)
  case SKIP
  then show ?case by auto
next
  case (Assign x a)
  thus ?case sorry
next
  case (Seq c1 c2)
  thus ?case sorry
next
  case (If x1 c1 c2)
  then show ?case sorry
next
  case (While x1 c)
  then show ?case sorry
qed

(*Theorem 8.19 (Compiler correctness).*)
theorem ccomp_exec: "ccomp c \<turnstile> (0,s,stk) \<rightarrow>* (size (ccomp c), t, stk) \<Longrightarrow> (c,s) \<Rightarrow> t"
  using ccomp_exec_n exec_eq_exec_n by auto

end

repo: ConcreteSemantics


text:
theory Submission
  imports Defs
begin

lemma fixp:
  fixes f :: "nat \<Rightarrow> nat"
  assumes incr: "\<forall>n. n \<le> f n"
  assumes A: "A = {m. \<exists>n. m = f n}"
  assumes max: "\<exists>m \<in> A. \<forall>n \<in> A. n \<le> m"
  shows "\<exists>k\<in>A. f k = k"
proof-
  from max obtain m where m_def: "\<forall>n \<in> A. n \<le> m" by auto
  then have "m \<le> f m" using incr by simp
  moreover from m_def A have "f m \<le> m" by blast
  ultimately have "m = f m" by auto
  then show "\<exists>k\<in>A. f k = k"
    using A by force
qed

end

author: MaximilianAnzinger


text:
(*  Title:      LList_Topology.thy
    Author:     Stefan Friedrich
    Maintainer: Stefan Friedrich
    License:    LGPL
*)

section \<open>The topology of llists\<close>

theory LList_Topology
imports Topology "Lazy-Lists-II.LList2"
begin

subsection\<open>The topology of all llists\<close>

text\<open>
  This theory introduces the topologies of all llists, of infinite
  llists, and of the non-empty llists. For all three cases it is
  proved that safety properties are closed sets and that liveness
  properties are dense sets. Finally, we prove in each of the the
  three different topologies the respective theorem of Alpern and
  Schneider \cite{alpern85:_defin_liven}, which states that every
  property can be represented as an intersection of a safety property
  and a liveness property.\<close>

definition
  ttop :: "'a set \<Rightarrow> 'a llist top" where
  "ttop A = topo (\<Union> s\<in>A\<^sup>\<star>. {suff A s})"

lemma ttop_topology [iff]: "topology (ttop A)"
  by (auto simp: ttop_def)

locale suffixes =
  fixes A and B
  defines [simp]: "B \<equiv> (\<Union> s\<in>A\<^sup>\<star>. {suff A s})"

locale trace_top = suffixes + topobase

lemma (in trace_top) open_iff [iff]:
  "m open = (m \<in> topo (\<Union> s\<in>A\<^sup>\<star>. {suff A s}))"
  by (simp add: T_def is_open_def)

lemma (in trace_top) suff_open [intro!]:
  "r \<in> A\<^sup>\<star> \<Longrightarrow> suff A r open"
  by auto

lemma (in trace_top) ttop_carrier: "A\<^sup>\<infinity> = carrier"
  by (auto simp: carrier_topo suff_def)

lemma (in trace_top) nhds_LNil [simp]: "nhds LNil = {A\<^sup>\<infinity>}"
proof
  show "nhds LNil \<subseteq> {A\<^sup>\<infinity>}"
  proof clarify
    fix x assume xnhd: "x \<in> nhds LNil"
    then obtain r
      where rfinpref: "r \<in> finpref A LNil" and suffsub: "suff A r \<subseteq> x"
      by (rule suff_nhd_base)
    from rfinpref have "r = LNil" by auto
    hence "suff A r = A\<^sup>\<infinity>" by auto
    with suffsub have "A\<^sup>\<infinity> \<subseteq> x" by auto
    moreover from xnhd have "x \<subseteq> A\<^sup>\<infinity>" by(auto simp: ttop_carrier elim!: nhdE)
    ultimately show "x = A\<^sup>\<infinity>" by auto
  qed
next
  show "{A\<^sup>\<infinity>} \<subseteq> nhds LNil" by (auto simp: ttop_carrier)
qed

lemma (in trace_top) adh_lemma:
assumes xpoint: "x \<in> A\<^sup>\<infinity>"
  and  PA: "P \<subseteq> A\<^sup>\<infinity>"
shows "(x adh P) = (\<forall> r \<in> finpref A x. \<exists> s \<in> A\<^sup>\<infinity>. r @@ s \<in> P)"
proof-
  from PA have "\<And>r. r \<in> A\<^sup>\<star> \<Longrightarrow> (\<exists> s \<in> A\<^sup>\<infinity>. r @@ s \<in> P) =
        (\<exists> s \<in> P. r \<le> s)"
    by (auto simp: llist_le_def iff: lapp_allT_iff)
  hence  "(\<forall> r \<in> finpref A x. \<exists> s \<in> A\<^sup>\<infinity>. r @@ s \<in> P) =
        (\<forall> r \<in> finpref A x. \<exists> s \<in> P. r \<le> s)"
    by (auto simp: finpref_def)
  also have "\<dots> = (\<forall> r \<in> finpref A x. suff A r \<inter> P \<noteq> {})"
  proof-
    have "\<And>r. (\<exists>s\<in>P. r \<le> s) = ({ra. ra \<in> A\<^sup>\<infinity> \<and> r \<le> ra} \<inter> P \<noteq> {})" using PA
      by blast
    thus ?thesis by (simp add: suff_def)
  qed
  also have "\<dots> = (\<forall> u \<in> nhds x. u \<inter> P \<noteq> {})"
  proof safe
    fix r assume uP: "\<forall>u\<in>nhds x. u \<inter> P \<noteq> {}" and
      rfinpref: "r \<in> finpref A x" and rP: "suff A r \<inter> P = {}"
    from rfinpref have "suff A r open" by (auto dest!: finpref_fin)
    hence "suff A r \<in> nhds x" using xpoint rfinpref
      by auto
    with uP rP show "False" by auto
  next
    fix u assume
      inter:     "\<forall>r\<in>finpref A x. suff A r \<inter> P \<noteq> {}" and
      unhd:   "u \<in> nhds x" and
      uinter: "u \<inter> P = {}"
    from unhd obtain r where
      "r \<in> finpref A x" and "suff A r \<subseteq> u"
      by (rule suff_nhd_base)
    with inter uinter show "False" by auto
  qed
  finally show ?thesis by (simp add: adhs_def)
qed

lemma (in trace_top) topology [iff]:
  "topology T"
by (simp add: T_def)

lemma (in trace_top) safety_closed_iff:
  "P \<subseteq> A\<^sup>\<infinity> \<Longrightarrow>  safety A P = (P closed)"
by (auto simp: safety_def topology.closed_adh adh_lemma ttop_carrier)

lemma (in trace_top) liveness_dense_iff:
  assumes P: "P \<subseteq> A\<^sup>\<infinity>"
  shows "liveness A P = (P dense)"
proof-
  have "liveness A P = (\<forall>r\<in>A\<^sup>\<star>. \<exists> s \<in> A\<^sup>\<infinity>. r @@ s \<in> P)"
    by (simp add: liveness_def)
  also have "\<dots> = (\<forall>x\<in>A\<^sup>\<infinity>. \<forall> r \<in> finpref A x. \<exists> s \<in> A\<^sup>\<infinity>. r @@ s \<in> P)"
      by (auto simp: finpref_def dest: finsubsetall)
  also have "\<dots> = (\<forall>x\<in>A\<^sup>\<infinity>. x adh P)" using P
    by (simp add: adh_lemma)
  also have "\<dots> = (A\<^sup>\<infinity> \<subseteq> closure P)" using P
    by (auto simp: adh_closure_iff ttop_carrier)
  also have "\<dots> = (P dense)"
    by (simp add: liveness_def is_dense_def is_densein_def ttop_carrier)
  finally show ?thesis .
qed

lemma (in trace_top) LNil_safety: "safety A {LNil}"
proof (unfold safety_def, clarify)
  fix t
  assume adh: "t \<in> A\<^sup>\<infinity>" "\<forall>r\<in>finpref A t. \<exists>s\<in>A\<^sup>\<infinity>. r @@ s \<in> {LNil}"
  thus "t = LNil" by (cases t)(auto simp: finpref_def)
qed

lemma (in trace_top) LNil_closed: "{LNil} closed"
by (auto intro: iffD1 [OF safety_closed_iff] LNil_safety)

theorem (in trace_top) alpern_schneider:
assumes Psub:     "P \<subseteq> A\<^sup>\<infinity>"
  shows "\<exists> S L. safety A S \<and> liveness A L \<and> P = S \<inter> L"
proof-
  from Psub have "P \<subseteq> carrier" by (simp add: ttop_carrier)
  then obtain L S where
    Lsub: "L \<subseteq> carrier" and
    Ssub: "S \<subseteq> carrier" and
    Sclosed: "S closed" and
    Ldense: "L dense" and
    Pinter: "P = S \<inter> L"
    by (blast elim: topology.ex_dense_closure_interE [OF topology])
  from Ssub Sclosed have "safety A S"
    by (simp add: safety_closed_iff ttop_carrier)
  moreover from Lsub Ldense have "liveness A L"
    by (simp add: liveness_dense_iff ttop_carrier)
  ultimately show ?thesis using Pinter
    by auto
qed

subsection\<open>The topology of infinite llists\<close>

definition
  itop :: "'a set \<Rightarrow> 'a llist top" where
  "itop A = topo (\<Union> s\<in>A\<^sup>\<star>. {infsuff A s})"

locale infsuffixes =
  fixes A and B
  defines [simp]: "B \<equiv> (\<Union> s\<in>A\<^sup>\<star>. {infsuff A s})"

locale itrace_top = infsuffixes + topobase

lemma (in itrace_top) open_iff [iff]:
  "m open = (m \<in> topo (\<Union> s\<in>A\<^sup>\<star>. {infsuff A s}))"
  by (simp add: T_def is_open_def)

lemma (in itrace_top) topology [iff]: "topology T"
  by (auto simp: T_def)

lemma (in itrace_top) infsuff_open [intro!]:
  "r \<in> A\<^sup>\<star> \<Longrightarrow> infsuff A r open"
  by auto

lemma (in itrace_top) itop_carrier: "carrier = A\<^sup>\<omega>"
  by (auto simp: carrier_topo infsuff_def)

lemma itop_sub_ttop_base:
  fixes A :: "'a set"
    and B :: "'a llist set set"
    and C :: "'a llist set set"
  defines [simp]: "B \<equiv> \<Union>s\<in>A\<^sup>\<star>. {suff A s}" and [simp]: "C \<equiv> \<Union>s\<in>A\<^sup>\<star>. {infsuff A s}"
  shows "C = (\<Union> t\<in>B. {t \<inter> \<Union>C})"
  by (auto simp: infsuff_def suff_def)

lemma itop_sub_ttop [folded ttop_def itop_def]:
  fixes A and C and S (structure)
  defines "C \<equiv> \<Union>s\<in>A\<^sup>\<star>. {infsuff A s}" and "S \<equiv> topo C"
  fixes B and T (structure)
  defines "B \<equiv> \<Union>s\<in>A\<^sup>\<star>. {suff A s}" and "T \<equiv> topo B"
  shows "subtopology S T"
proof -
  interpret itrace_top A C S by fact+
  interpret trace_top A B T by fact+
  show ?thesis
    by (auto intro: itop_sub_ttop_base [THEN subtop_lemma] simp: S_def T_def)
qed

lemma (in itrace_top) infsuff_nhd_base:
  assumes unhd: "u \<in> nhds t"
  and H: "\<And>r. \<lbrakk> r \<in> finpref A t; infsuff A r \<subseteq> u \<rbrakk> \<Longrightarrow> R"
  shows "R"
proof-
  from unhd obtain m where
    uA: "u \<subseteq> A\<^sup>\<omega>" and
    mopen: "m open" and
    tm: "t \<in> m" and
    mu: "m \<subseteq> u"
    by (auto simp: itop_carrier)
  from mopen tm have
    "\<exists>r \<in> finpref A t. infsuff A r \<subseteq> m"
  proof (induct "m")
    case (basic a)
    then obtain s where sA: "s \<in> A\<^sup>\<star>" and as: "a = infsuff A s" and ta: "t \<in> a"
      by auto
    from sA as ta have "s \<in> finpref A t" by (auto dest: infsuff_finpref)
    thus ?case using as by auto
  next case (inter a b)
    then obtain r r' where
      rt: "r \<in> finpref A t" and ra: "infsuff A r \<subseteq> a" and
      r't: "r' \<in> finpref A t" and r'b: "infsuff A r' \<subseteq> b"
      by auto
    from rt r't have "r \<le> r' \<or> r' \<le> r"
      by (auto simp: finpref_def dest: pref_locally_linear)
    thus ?case
    proof
      assume "r \<le> r'"
      hence "infsuff A r' \<subseteq> infsuff A r" by (rule infsuff_mono2)
      thus ?case using r't ra r'b by auto
    next assume "r' \<le> r"
      hence "infsuff A r \<subseteq> infsuff A r'" by (rule infsuff_mono2)
      thus ?case using rt r'b ra by auto
    qed
  next case (union M)
    then obtain v where
      "t \<in> v" and vM: "v \<in> M"
      by blast
    then obtain r where "r\<in>finpref A t" "infsuff A r \<subseteq> v" using union
      by auto
    thus ?case using vM by auto
  qed
  with mu show ?thesis by (auto intro: H)
qed

lemma (in itrace_top) hausdorff [iff]: "T2 T"
proof(rule T2I, clarify)
  fix x y assume xpoint: "x \<in> carrier"
    and ypoint: "y \<in> carrier"
    and neq: "x \<noteq> y"
  from xpoint ypoint have xA: "x \<in> A\<^sup>\<omega>" and yA: "y \<in> A\<^sup>\<omega>"
    by (auto simp: itop_carrier)
  then obtain s where
    sA: "s \<in> A\<^sup>\<star>" and sx: "s \<le> x" and sy: "\<not> s \<le> y" using neq
    by (rule inf_neqE) auto
  from neq have "y \<noteq> x" ..
  with yA xA obtain t where
    tA: "t \<in> A\<^sup>\<star>" and ty: "t \<le> y" and tx: "\<not> t \<le> x"
    by (rule inf_neqE) auto
  let ?u = "infsuff A s" and ?v = "infsuff A t"
  have inter: "?u \<inter> ?v = {}"
  proof (rule ccontr, auto)
    fix z assume "z \<in> ?u" and "z \<in> ?v"
    hence "s \<le> z" and  "t \<le> z" by (unfold infsuff_def) auto
    hence "s \<le> t \<or> t \<le> s" by (rule pref_locally_linear)
    thus False using sx sy tx ty by (auto dest: llist_le_trans)
  qed
  moreover {
    from sA tA have "?u open" and "?v open"
      by auto
    moreover from xA yA sx ty have "x \<in> ?u" and "y \<in> ?v"
      by (auto simp: infsuff_def)
    ultimately have "infsuff A s \<in> nhds x" and
      "infsuff A t \<in> nhds y"
      by auto }
  ultimately show "\<exists> u \<in> nhds x. \<exists> v \<in> nhds y. u \<inter> v = {}"
    by auto
qed

corollary (in itrace_top) unique_convergence:
  "\<lbrakk> x \<in> carrier;
     y \<in> carrier;
     F \<in> Filters ;
     F \<longlongrightarrow> x;
     F \<longlongrightarrow> y \<rbrakk> \<Longrightarrow> x = y"
  apply (rule T2.unique_convergence)
  prefer 2
  apply (rule filter.intro)
  apply auto
  done

(*
lemma safty_closed:
  fixes   A :: "'a set"
  defines "T \<equiv> itop A"
  assumes P: "P \<subseteq> A\<^sup>\<omega>"
  and safety: "safety A P"
  shows "P iscl T"
proof-
  have istopT [iff]: "istop T" by (simp add: T_def)
  have carrT [simp]: "carr T = A\<^sup>\<omega>" by (simp add: T_def itop_carr)
  show ?thesis
  proof (rule closure_eq_closed, auto)
    fix x assume xclos: "x \<in> clos T P"
    with P have "x \<in> carr T"
      by (intro subsetD [OF closure_subset]) auto
    hence xA: "x \<in> A\<^sup>\<omega>" by simp
    moreover
    from P xclos have adhx: "adh T P x" by (auto intro!: closure_imp_adh)
    have "\<forall> r \<in> finpref A x. \<exists> s \<in> A\<^sup>\<omega>. r @@ s \<in> P"
    proof
      fix r assume "r \<in> finpref A x"
      hence "x \<in> infsuff A r" and rA: "r \<in> A\<^sup>\<star>" using xA
        by (auto simp: finpref_def infsuff_def)
      hence "infsuff A r \<in> nhds T x" by (auto simp: T_def)
      with adhx have  "infsuff A r \<inter> P \<noteq> {}" by (elim adhCE) auto
      then obtain t where "t \<in> infsuff A r" and tP: "t \<in> P" by auto
      then obtain s where "s \<in> A\<^sup>\<omega>" and "t = r @@ s" using rA
        by (auto elim!: infsuff_appE)
      thus "\<exists> s \<in> A\<^sup>\<omega>. r @@ s \<in> P" using tP by auto
    qed
    ultimately show "x \<in> P" using safety
      by (auto elim: safetyE)
  qed
qed
*)
lemma (in itrace_top) adh_lemma:
assumes xpoint: "x \<in> A\<^sup>\<omega>"
  and  PA: "P \<subseteq> A\<^sup>\<omega>"
shows "x adh P = (\<forall> r \<in> finpref A x. \<exists> s \<in> A\<^sup>\<omega>. r @@ s \<in> P)"
proof-
  from PA have "\<And>r. r \<in> A\<^sup>\<star> \<Longrightarrow> (\<exists> s \<in> A\<^sup>\<omega>. r @@ s \<in> P) =
        (\<exists> s \<in> P. r \<le> s)"
    by (auto simp: llist_le_def iff: lapp_infT)
  hence  "(\<forall> r \<in> finpref A x. \<exists> s \<in> A\<^sup>\<omega>. r @@ s \<in> P) =
        (\<forall> r \<in> finpref A x. \<exists> s \<in> P. r \<le> s)"
    by (auto simp: finpref_def)
  also have "\<dots> = (\<forall> r \<in> finpref A x. infsuff A r \<inter> P \<noteq> {})"
  proof-
    have "\<And>r. (\<exists>s\<in>P. r \<le> s) = ({ra. ra \<in> A\<^sup>\<omega> \<and> r \<le> ra} \<inter> P \<noteq> {})" using PA
      by blast
    thus ?thesis by (simp add: infsuff_def)
  qed
  also have "\<dots> = (\<forall> u \<in> nhds x. u \<inter> P \<noteq> {})"
  proof safe
    fix r assume uP: "\<forall> u \<in> nhds x. u \<inter> P \<noteq> {}" and
      rfinpref: "r \<in> finpref A x" and rP: "infsuff A r \<inter> P = {}"
    from rfinpref have "infsuff A r open" by (auto dest!: finpref_fin)
    hence "infsuff A r \<in> nhds x" using xpoint rfinpref
      by auto
    with uP rP show "False" by auto
  next
    fix u assume
      inter:     "\<forall>r\<in>finpref A x. infsuff A r \<inter> P \<noteq> {}" and
      unhd:   "u \<in> nhds x" and
      uinter: "u \<inter> P = {}"
    from unhd obtain r where
      "r \<in> finpref A x" and "infsuff A r \<subseteq> u"
      by (rule infsuff_nhd_base)
    with inter uinter show "False" by auto
  qed
  finally show ?thesis by (simp add: adhs_def)
qed

lemma (in itrace_top) infsafety_closed_iff:
  "P \<subseteq> A\<^sup>\<omega> \<Longrightarrow>  infsafety A P = (P closed)"
  by (auto simp: infsafety_def topology.closed_adh adh_lemma itop_carrier)

lemma (in itrace_top) empty:
  "A = {} \<Longrightarrow> T = {{}}"
proof (auto simp: T_def)
  fix m x assume "m \<in> topo {{}}" and  xm: "x \<in> m"
  thus False
    by (induct m) auto
qed

lemma itop_empty: "itop {} = {{}}"
proof (auto simp: itop_def)
  fix m x assume "m \<in> topo {{}}" and  xm: "x \<in> m"
  thus False
    by (induct m) auto
qed

lemma infliveness_empty:
  "infliveness {} P \<Longrightarrow> False"
  by (auto simp: infliveness_def)

lemma (in trivial) dense:
  "P dense"
  by auto

lemma (in itrace_top) infliveness_dense_iff:
  assumes notempty: "A \<noteq> {}"
  and P: "P \<subseteq> A\<^sup>\<omega>"
  shows "infliveness A P = (P dense)"
proof-
  have "infliveness A P = (\<forall>r\<in>A\<^sup>\<star>. \<exists> s \<in> A\<^sup>\<omega>. r @@ s \<in> P)"
    by (simp add: infliveness_def)
  also have "\<dots> = (\<forall>x\<in>A\<^sup>\<omega>. \<forall> r \<in> finpref A x. \<exists> s \<in> A\<^sup>\<omega>. r @@ s \<in> P)"
  proof-
    from notempty obtain a where "a \<in> A"
      by auto
    hence lc: "lconst a \<in> A\<^sup>\<omega>"
      by (rule lconstT)
    hence "\<And>P. (\<forall>x\<in>A\<^sup>\<omega>. \<forall>r\<in>finpref A x. P r) = (\<forall> r\<in>A\<^sup>\<star>. P r)"
    proof (auto dest: finpref_fin)
      fix P r  assume lc: "lconst a \<in> A\<^sup>\<omega>"
        and Pr: "\<forall>x\<in>A\<^sup>\<omega>. \<forall>r\<in>finpref A x. P r"
        and rA: "r \<in> A\<^sup>\<star>"
      from rA lc have rlc: "r @@ lconst a \<in> A\<^sup>\<omega>" by (rule lapp_fin_infT)
      moreover from rA rlc have "r \<in> finpref A (r @@ lconst a)"
        by (auto simp: finpref_def llist_le_def)
      ultimately show "P r" using Pr by auto
    qed
    thus ?thesis by simp
  qed
  also have "\<dots> = (\<forall>x\<in>A\<^sup>\<omega>. x adh P)" using P
    by (simp add: adh_lemma)
  also have "\<dots> = (A\<^sup>\<omega> \<subseteq> closure P)" using P
    by (auto simp: adh_closure_iff itop_carrier)
  also have "\<dots> = (P dense)"
    by (simp add: infliveness_def is_dense_def is_densein_def itop_carrier)
  finally show ?thesis .
qed

theorem (in itrace_top) alpern_schneider:
assumes notempty: "A \<noteq> {}"
  and   Psub:     "P \<subseteq> A\<^sup>\<omega>"
  shows "\<exists> S L. infsafety A S \<and> infliveness A L \<and> P = S \<inter> L"
proof-
  from Psub have "P \<subseteq> carrier"
    by (simp add: itop_carrier [THEN sym])
  then obtain L S where
    Lsub: "L \<subseteq> carrier" and
    Ssub: "S \<subseteq> carrier" and
    Sclosed: "S closed" and
    Ldense: "L dense" and
    Pinter: "P = S \<inter> L"
    by (rule topology.ex_dense_closure_interE [OF topology]) auto
  from Ssub Sclosed have "infsafety A S"
    by (simp add: infsafety_closed_iff itop_carrier)
  moreover from notempty Lsub Ldense have "infliveness A L"
    by (simp add: infliveness_dense_iff itop_carrier)
  ultimately show ?thesis using Pinter
    by auto
qed

subsection\<open>The topology of non-empty llists\<close>

definition
  ptop :: "'a set \<Rightarrow> 'a llist top" where
  "ptop A \<equiv> topo (\<Union> s\<in>A\<^sup>\<clubsuit>. {suff A s})"

locale possuffixes =
  fixes A and B
  defines [simp]: "B \<equiv> (\<Union> s\<in>A\<^sup>\<clubsuit>. {suff A s})"

locale ptrace_top = possuffixes + topobase

lemma (in ptrace_top) open_iff [iff]:
  "m open = (m \<in> topo (\<Union> s\<in>A\<^sup>\<clubsuit>. {suff A s}))"
  by (simp add: T_def is_open_def)

lemma (in ptrace_top) topology [iff]: "topology T"
  by (simp add: T_def)

lemma (in ptrace_top) ptop_carrier: "carrier = A\<^sup>\<spadesuit>"
by (auto simp add: carrier_topo suff_def)
   (auto elim: alllsts.cases)

lemma pptop_subtop_ttop:
  fixes S (structure)
  fixes A and B and T (structure)
  defines "B \<equiv> \<Union>s\<in>A\<^sup>\<star>. {suff A s}" and "T \<equiv> topo B"
  defines "S \<equiv> \<Union> t \<in> T. {t - {LNil}}"
  shows "subtopology S T"
by (rule subtopology.intro, auto simp add: is_open_def S_def carr_def)

lemma pptop_top:
  fixes S (structure)
  fixes A and B and T (structure)
  defines "B \<equiv> \<Union>s\<in>A\<^sup>\<star>. {suff A s}" and "T \<equiv> topo B"
  defines "S \<equiv> \<Union> t \<in> T. {t - {LNil}}"
  shows  "topology (\<Union> t \<in> T. {t - {LNil}})"
proof -
  interpret trace_top A B T by fact+
  show ?thesis
    by (auto intro!: subtopology.subtop_topology [OF pptop_subtop_ttop]
      trace_top.topology simp: T_def)
qed

(*
lemma
  includes ptrace_top A B S
  includes trace_top  A C T
  fixes S' (structure)
  defines  "S' \<equiv> (\<Union> t \<in> T. {t - {LNil}})"
  shows "S = S'"
proof-
  have [iff]: "\<And> m. m open\<^sub>3 = (\<exists>t. t open\<^sub>2 \<and> m = t - {LNil})"
    by (auto simp add: S'_def is_open_def)
  show ?thesis
  proof
    fix m assume "m open"
    thus "m open\<^sub>3"
    proof (induct m)
      case (basic m) thus ?case by auto
    next case (inter u v) thus ?case
        by (blast intro: topology.Int_open [OF pptop_top])
    next case (union M) thus ?case
        by (auto intro!: topology.union_open [OF pptop_top] simp: S'_def T_def)
    qed
  next
    fix m assume "m open\<^sub>3"
    then obtain t where "t open\<^sub>2" and mt: "m = t - {LNil}" by auto
    hence "t - {LNil} open\<^sub>1"
    proof (induct t)
      case (basic x)
      then obtain s where sfin: "s \<in> A\<^sup>\<star>" and
        ms: "x = suff A s"
        by auto
      thus ?case
      proof (cases s)
        case LNil_fin with ms
        have "x - {LNil} = carrier" by (auto simp: ptop_carrier)
        thus ?thesis by (auto intro!: topology.carrier_open [OF pptop_top])
      next
        case (LCons_fin a l) with ms show ?thesis
          by (auto simp: ptop_def)
      qed
    next case (inter u v)
      hence "(u - {LNil}) \<inter> (v - {LNil}) \<in> ptop A" by auto
      moreover have "(u - {LNil}) \<inter> (v - {LNil}) = (u \<inter> v) - {LNil}"
        by auto
      ultimately show ?case by auto
    next case (union M)
      hence "\<Union>{u. \<exists>x\<in>M. u = x - {LNil}} \<in> ptop A" by auto
      moreover have "\<Union>{u. \<exists>x\<in>M. u = x - {LNil}} = \<Union>M - {LNil}" by auto
      ultimately show ?case by auto
    qed
    thus "x \<in> ptop A" using xt by auto
  qed
qed
*)
lemma (in ptrace_top) suff_open [intro!]:
  "r \<in> A\<^sup>\<clubsuit> \<Longrightarrow> suff A r open"
  by auto

lemma (in ptrace_top) suff_ptop_nhd_base:
  assumes unhd: "u \<in> nhds t"
  and H: "\<And>r. \<lbrakk> r \<in> pfinpref A t; suff A r \<subseteq> u \<rbrakk> \<Longrightarrow> R"
  shows "R"
proof-
  from unhd obtain m where
    uA: "u \<subseteq> A\<^sup>\<spadesuit>" and
    mopen: "m open" and
    tm: "t \<in> m" and
    mu: "m \<subseteq> u"
    by (auto simp: ptop_carrier)
  from mopen tm have
    "\<exists>r \<in> pfinpref A t. suff A r \<subseteq> m"
  proof (induct "m")
    case (basic a)
    then obtain s where sA: "s \<in> A\<^sup>\<clubsuit>" and as: "a = suff A s" and ta: "t \<in> a"
      by auto
    from sA as ta have "s \<in> pfinpref A t"
      by (auto simp: pfinpref_def dest: suff_finpref)
    thus ?case using as by auto
  next case (inter a b)
    then obtain r r' where
      rt: "r \<in> pfinpref A t" and ra: "suff A r \<subseteq> a" and
      r't: "r' \<in> pfinpref A t" and r'b: "suff A r' \<subseteq> b"
      by auto
    from rt r't have "r \<le> r' \<or> r' \<le> r"
      by (auto simp: pfinpref_def finpref_def dest: pref_locally_linear)
    thus ?case
    proof
      assume "r \<le> r'"
      hence "suff A r' \<subseteq> suff A r" by (rule suff_mono2)
      thus ?case using r't ra r'b by auto
    next assume "r' \<le> r"
      hence "suff A r \<subseteq> suff A r'" by (rule suff_mono2)
      thus ?case using rt r'b ra by auto
    qed
  next case (union M)
    then obtain v where
      "t \<in> v" and vM: "v \<in> M"
      by blast
    then obtain r where "r\<in>pfinpref A t" "suff A r \<subseteq> v" using union
      by auto
    thus ?case using vM by auto
  qed
  with mu show ?thesis by (auto intro: H)
qed

lemma pfinpref_LNil [simp]: "pfinpref A LNil = {}"
  by (auto simp: pfinpref_def)

lemma (in ptrace_top) adh_lemma:
  assumes xpoint: "x \<in> A\<^sup>\<spadesuit>"
  and  P_subset_A: "P \<subseteq> A\<^sup>\<spadesuit>"
  shows "x adh P = (\<forall> r \<in> pfinpref A x. \<exists> s \<in> A\<^sup>\<infinity>. r @@ s \<in> P)"
proof
  assume adh_x: "x adh P"
  show "\<forall>r\<in>pfinpref A x. \<exists>s\<in>A\<^sup>\<infinity>. r @@ s \<in> P"
  proof
    fix r let ?u = "suff A r"
    assume r_pfinpref_x: "r \<in> pfinpref A x"
    hence r_pos: "r \<in> A\<^sup>\<clubsuit>" by (auto dest: finpref_fin)
    hence "?u open" by auto
    hence "?u \<in> nhds x" using xpoint r_pfinpref_x
      by auto
    with adh_x have  "?u \<inter> P \<noteq> {}" by (auto elim!:adhCE)
    then obtain t where tu: "t \<in> ?u" and tP: "t \<in> P"
      by auto
    from tu obtain s where "t = r @@ s" using r_pos
      by (auto elim!: suff_appE)
    with tP show "\<exists>s\<in>A\<^sup>\<infinity>. r @@ s \<in> P" using P_subset_A r_pos
      by (auto iff: lapp_allT_iff)
  qed
next
  assume H: "\<forall>r\<in>pfinpref A x. \<exists>s\<in>A\<^sup>\<infinity>. r @@ s \<in> P"
  show "x adh P"
  proof
    fix U assume unhd: "U \<in> nhds x"
    then obtain r where r_pfinpref_x: "r \<in> pfinpref A x" and
      suff_subset_U: "suff A r \<subseteq> U" by (elim suff_ptop_nhd_base)
    from r_pfinpref_x have rpos: "r \<in> A\<^sup>\<clubsuit>" by (auto intro: finpref_fin)
    show "U \<inter> P \<noteq> {}" using rpos
    proof (cases r)
      case (LCons a l)
      hence r_pfinpref_x: "r \<in> pfinpref A x" using r_pfinpref_x
        by auto
      with H obtain s where sA: "s \<in> A\<^sup>\<infinity>" and asP: "r@@s \<in> P"
        by  auto
      moreover have "r @@ s \<in> suff A r" using sA rpos
        by (auto simp: suff_def iff: lapp_allT_iff)
      ultimately show ?thesis using suff_subset_U by auto
    qed
  qed
qed

lemma (in ptrace_top) possafety_closed_iff:
  "P \<subseteq> A\<^sup>\<spadesuit> \<Longrightarrow>  possafety A P = (P closed)"
  by (auto simp: possafety_def topology.closed_adh ptop_carrier adh_lemma)
(*
lemma ptop_empty: "ptop {} = {{}}"
proof (auto simp: ptop_def intro!: topobase.basic)
  fix m x assume "m \<in> topo {}" and  xm: "x \<in> m"
  thus False
    by (induct m) auto
qed

lemma posliveness_empty:
  "posliveness {} P"
  by (auto simp: posliveness_def)
*)

lemma (in ptrace_top) posliveness_dense_iff:
  assumes P: "P \<subseteq> A\<^sup>\<spadesuit>"
  shows "posliveness A P = (P dense)"
proof-
  have "posliveness A P = (\<forall>r\<in>A\<^sup>\<clubsuit>. \<exists> s \<in> A\<^sup>\<infinity>. r @@ s \<in> P)"
    by (simp add: posliveness_def)
  also have "\<dots> = (\<forall>x\<in>A\<^sup>\<spadesuit>. \<forall> r \<in> pfinpref A x. \<exists> s \<in> A\<^sup>\<infinity>. r @@ s \<in> P)"
      by (auto simp: pfinpref_def finpref_def dest: finsubsetall)
  also have "\<dots> = (\<forall>x\<in>A\<^sup>\<spadesuit>. x adh P)" using P
    by (auto simp: adh_lemma simp del: poslsts_iff)
  also have "\<dots> = (A\<^sup>\<spadesuit> \<subseteq> closure P)" using P
    by (auto simp: adh_closure_iff ptop_carrier simp del: poslsts_iff)
  also have "\<dots> = (P dense)"
    by (simp add: posliveness_def is_dense_def is_densein_def ptop_carrier)
  finally show ?thesis .
qed

theorem (in ptrace_top) alpern_schneider:
assumes Psub: "P \<subseteq> A\<^sup>\<spadesuit>"
  shows "\<exists> S L. possafety A S \<and> posliveness A L \<and> P = S \<inter> L"
proof-
  from Psub have "P \<subseteq> carrier" by (simp add: ptop_carrier)
  then obtain L S where
    Lsub: "L \<subseteq> carrier" and
    Ssub: "S \<subseteq> carrier" and
    Sclosed: "S closed" and
    Ldense: "L dense" and
    Pinter: "P = S \<inter> L"
    by (blast elim: topology.ex_dense_closure_interE [OF topology])
  from Ssub Sclosed have "possafety A S"
    by (simp add: possafety_closed_iff ptop_carrier)
  moreover from Lsub Ldense have "posliveness A L"
    by (simp add: posliveness_dense_iff ptop_carrier)
  ultimately show ?thesis using Pinter
    by auto
qed

end

repo: PSL


text:
(*  Title:       Isabelle Collections Library
    Author:      Peter Lammich <peter dot lammich at uni-muenster.de>
    Maintainer:  Peter Lammich <peter dot lammich at uni-muenster.de>
*)
header {* \isaheader{Map Implementation by Association Lists with explicit invariants} *}
theory ListMapImpl_Invar
imports
  "../spec/MapSpec"
  "../../Lib/Assoc_List"
  "../gen_algo/MapGA"
begin
text_raw {*\label{thy:ListMapImpl_Invar}*}

(*@impl Map
  @type 'a lmi
  @abbrv lmi,l
  Maps implemented by associative lists. Version with explicit
  invariants that allows for efficient xxx-dj operations.
*)

type_synonym ('k,'v) lmi = "('k\<times>'v) list"

term revg

definition "lmi_\<alpha> \<equiv> Map.map_of"
definition "lmi_invar \<equiv> \<lambda>m. distinct (List.map fst m)"

definition lmi_basic_ops :: "('k,'v,('k,'v) lmi) map_basic_ops"
  where [icf_rec_def]: "lmi_basic_ops \<equiv> \<lparr>
  bmap_op_\<alpha> = lmi_\<alpha>,
  bmap_op_invar = lmi_invar,
  bmap_op_empty = (\<lambda>_::unit. []),
  bmap_op_lookup = (\<lambda>k m. Map.map_of m k),
  bmap_op_update = AList.update,
  bmap_op_update_dj = (\<lambda>k v m. (k, v) # m),
  bmap_op_delete = Assoc_List.delete_aux,
  bmap_op_list_it = foldli
\<rparr>"

setup Locale_Code.open_block
interpretation lmi_basic!: StdBasicMapDefs lmi_basic_ops .
interpretation lmi_basic!: StdBasicMap lmi_basic_ops
  unfolding lmi_basic_ops_def
  apply unfold_locales
  apply (simp_all
    add: icf_rec_unf lmi_\<alpha>_def lmi_invar_def
    add: AList.update_conv' AList.distinct_update Assoc_List.map_of_delete_aux'
      map_iterator_foldli_correct dom_map_of_conv_image_fst
  )
  done
setup Locale_Code.close_block

definition [icf_rec_def]: "lmi_ops \<equiv> lmi_basic.dflt_ops \<lparr>
  map_op_add_dj := revg,
  map_op_to_list := id,
  map_op_size := length,
  map_op_isEmpty := case_list True (\<lambda>_ _. False),
  map_op_isSng := (\<lambda>l. case l of [_] \<Rightarrow> True | _ \<Rightarrow> False)
\<rparr>"

setup Locale_Code.open_block
interpretation lmi!: StdMapDefs lmi_ops .
interpretation lmi!: StdMap lmi_ops
proof -
  interpret aux!: StdMap lmi_basic.dflt_ops by (rule lmi_basic.dflt_ops_impl)

  have [simp]: "map_add_dj lmi_\<alpha> lmi_invar revg"
    apply (unfold_locales)
    apply (auto simp: lmi_\<alpha>_def lmi_invar_def)
    apply (blast intro: map_add_comm)
    apply (simp add: rev_map[symmetric])
    apply fastforce
    done

  have [simp]: "map_to_list lmi_\<alpha> lmi_invar id"
    apply unfold_locales
    by (simp_all add: lmi_\<alpha>_def lmi_invar_def)

  have [simp]: "map_isEmpty lmi_\<alpha> lmi_invar (case_list True (\<lambda>_ _. False))"
    apply unfold_locales
    unfolding lmi_\<alpha>_def lmi_invar_def
    by (simp split: list.split)

  have [simp]: "map_isSng lmi_\<alpha> lmi_invar
     (\<lambda>l. case l of [_] \<Rightarrow> True | _ \<Rightarrow> False)"
    apply unfold_locales
    unfolding lmi_\<alpha>_def lmi_invar_def
    apply (auto split: list.split)
    apply (metis (no_types) map_upd_nonempty)
    by (metis fun_upd_other fun_upd_same option.simps(3))

  have [simp]: "map_size_axioms lmi_\<alpha> lmi_invar length"
    apply unfold_locales
    unfolding lmi_\<alpha>_def lmi_invar_def
    by (metis card_dom_map_of)

  show "StdMap lmi_ops"
    unfolding lmi_ops_def
    apply (rule StdMap_intro)
    apply (simp_all)
    apply intro_locales
    apply (simp_all add: icf_rec_unf)
    done
qed
setup Locale_Code.close_block

setup {* ICF_Tools.revert_abbrevs "lmi"*}

lemma pi_lmi[proper_it]:
  "proper_it' foldli foldli"
  by (intro proper_it'I icf_proper_iteratorI)

interpretation pi_lmi: proper_it_loc foldli foldli
  apply unfold_locales
  apply (rule pi_lmi)
  done

definition lmi_from_list_dj :: "('k\<times>'v) list \<Rightarrow> ('k,'v) lmi" where
  "lmi_from_list_dj \<equiv> id"

lemma lmi_from_list_dj_correct:
  assumes [simp]: "distinct (map fst l)"
  shows "lmi.\<alpha> (lmi_from_list_dj l) = map_of l"
        "lmi.invar (lmi_from_list_dj l)"
  by (auto simp add: lmi_from_list_dj_def icf_rec_unf lmi_\<alpha>_def lmi_invar_def)

text {* Code generator test *}
definition "test_codegen \<equiv> (
  lmi.add ,
  lmi.add_dj ,
  lmi.ball ,
  lmi.bex ,
  lmi.delete ,
  lmi.empty ,
  lmi.isEmpty ,
  lmi.isSng ,
  lmi.iterate ,
  lmi.iteratei ,
  lmi.list_it ,
  lmi.lookup ,
  lmi.restrict ,
  lmi.sel ,
  lmi.size ,
  lmi.size_abort ,
  lmi.sng ,
  lmi.to_list ,
  lmi.to_map ,
  lmi.update ,
  lmi.update_dj,
  lmi_from_list_dj
  )"

export_code test_codegen in SML

end

author: Josh-Tilles

repo: AFP

save_path: github-repos/isabelle/Josh-Tilles-AFP


text:
(* Authors: Lammich, Wimmer *)
theory Worklist_Subsumption1
  imports Worklist_Subsumption_Multiset
begin

subsection \<open>From Multisets to Lists\<close>

subsubsection \<open>Utilities\<close>

definition take_from_list where
  "take_from_list s = ASSERT (s \<noteq> []) \<then> SPEC (\<lambda> (x, s'). s = x # s')"

lemma take_from_list_correct:
  assumes "s \<noteq> []"
  shows "take_from_list s \<le> SPEC (\<lambda> (x, s'). s = x # s')"
using assms unfolding take_from_list_def by simp

lemmas [refine_vcg] = take_from_list_correct[THEN order.trans]

context Search_Space_Defs_Empty
begin

  definition "worklist_inv_frontier_list passed wait =
    (\<forall> a \<in> passed. \<forall> a'. E a a' \<and> \<not> empty a' \<longrightarrow> (\<exists> b' \<in> passed \<union> set wait. a' \<preceq> b'))"

  definition "start_subsumed_list passed wait = (\<exists> a \<in> passed \<union> set wait. a\<^sub>0 \<preceq> a)"

  definition "worklist_inv_list \<equiv> \<lambda> (passed, wait, brk).
    passed \<subseteq> Collect reachable \<and>
    (brk \<longrightarrow> (\<exists> f. reachable f \<and> F f)) \<and>
    (\<not> brk \<longrightarrow>
      worklist_inv_frontier_list passed wait
    \<and> (\<forall> a \<in> passed \<union> set wait. \<not> F a)
    \<and> start_subsumed_list passed wait
    \<and> set wait \<subseteq> Collect reachable)
    \<and> (\<forall> a \<in> passed. \<not> empty a) \<and> (\<forall> a \<in> set wait. \<not> empty a)
    "

  definition "add_succ_spec_list wait a \<equiv> SPEC (\<lambda>(wait',brk).
    (
    if \<exists>a'. E a a' \<and> F a' then
      brk
    else
      \<not>brk \<and> set wait' \<subseteq> set wait \<union> {a' . E a a'} \<and>
      (\<forall> s \<in> set wait \<union> {a' . E a a' \<and> \<not> empty a'}. \<exists> s' \<in> set wait'. s \<preceq> s')
    ) \<and> (\<forall> s \<in> set wait'. \<not> empty s)
  )"

end \<comment> \<open>Search Space Empty Defs\<close>

context Search_Space''_Defs
begin
  definition worklist_algo_list where
    "worklist_algo_list = do
      {
        if F a\<^sub>0 then RETURN True
        else do {
          let passed = {};
          let wait = [a\<^sub>0];
          (passed, wait, brk) \<leftarrow> WHILEIT worklist_inv_list (\<lambda> (passed, wait, brk). \<not> brk \<and> wait \<noteq> [])
            (\<lambda> (passed, wait, brk). do
              {
                (a, wait) \<leftarrow> take_from_list wait;
                ASSERT (reachable a);
                if (\<exists> a' \<in> passed. a \<unlhd> a') then RETURN (passed, wait, brk) else
                do
                  {
                    (wait,brk) \<leftarrow> add_succ_spec_list wait a;
                    let passed = insert a passed;
                    RETURN (passed, wait, brk)
                  }
              }
            )
            (passed, wait, False);
            RETURN brk
        }
      }
    "

end \<comment> \<open>Search Space'' Defs\<close>

context Search_Space''_pre
begin

  lemma worklist_algo_list_inv_ref:
    fixes x x'
    assumes
      "\<not> F a\<^sub>0" "\<not> F a\<^sub>0"
      "(x, x') \<in> {((passed,wait,brk), (passed',wait',brk')). passed = passed' \<and> mset wait = wait' \<and> brk = brk' }"
      "worklist_inv' x'"
    shows "worklist_inv_list x"
    using assms
    unfolding worklist_inv'_def worklist_inv_def worklist_inv_list_def
    unfolding worklist_inv_frontier_def worklist_inv_frontier_list_def
    unfolding worklist_start_subsumed_def start_subsumed_list_def
    by auto

  lemma take_from_list_take_from_mset_ref[refine]:
    "take_from_list xs \<le> \<Down> {((x, xs),(y, m)). x = y \<and> mset xs = m} (take_from_mset m)"
    if "mset xs = m"
    using that unfolding take_from_list_def take_from_mset_def
    by (clarsimp simp: pw_le_iff refine_pw_simps)

  lemma add_succ_spec_list_add_succ_spec_ref[refine]:
    "add_succ_spec_list xs b \<le> \<Down> {((xs, b), (m, b')). mset xs = m \<and> b = b'} (add_succ_spec' m b')"
    if "mset xs = m" "b = b'"
    using that unfolding add_succ_spec_list_def add_succ_spec'_def
    by (clarsimp simp: pw_le_iff refine_pw_simps)

  lemma worklist_algo_list_ref[refine]: "worklist_algo_list \<le> \<Down>Id worklist_algo'"
    unfolding worklist_algo_list_def worklist_algo'_def
    apply (refine_rcg)
               apply blast
              prefer 2
              apply (rule worklist_algo_list_inv_ref; assumption)
    by auto

end \<comment> \<open>Search Space''\<close>

subsection \<open>Towards an Implementation\<close>
context Worklist1_Defs
begin

  definition
    "add_succ1 wait a \<equiv>
     nfoldli (succs a) (\<lambda>(_,brk). \<not>brk)
      (\<lambda>a (wait,brk).
        do {
        ASSERT (\<forall> x \<in> set wait. \<not> empty x);
        if F a then RETURN (wait,True) else RETURN (
          if (\<exists> x \<in> set wait. a \<preceq> x \<and> \<not> x \<preceq> a) \<or> empty a
          then [x \<leftarrow> wait. \<not> x \<preceq> a]
          else a # [x \<leftarrow> wait. \<not> x \<preceq> a],False)
        }
      )
      (wait,False)"

end

context Worklist2_Defs
begin

  definition
    "add_succ1' wait a \<equiv>
     nfoldli (succs a) (\<lambda>(_,brk). \<not>brk)
      (\<lambda>a (wait,brk).
        if F a then RETURN (wait,True) else RETURN (
          if empty a
          then wait
          else if \<exists> x \<in> set wait. a \<unlhd> x \<and> \<not> x \<unlhd> a
          then [x \<leftarrow> wait. \<not> x \<unlhd> a]
          else a # [x \<leftarrow> wait. \<not> x \<unlhd> a],False)
      )
      (wait,False)"

end

context Worklist1
begin

lemma add_succ1_ref[refine]:
  "add_succ1 wait a \<le> \<Down>(Id \<times>\<^sub>r bool_rel) (add_succ_spec_list wait' a')"
  if "(wait,wait')\<in>Id" "(a,a')\<in>b_rel Id reachable" "\<forall> x \<in> set wait'. \<not> empty x"
  using that
  apply simp
  unfolding add_succ_spec_list_def add_succ1_def
  apply (refine_vcg nfoldli_rule[where I =
        "\<lambda>l1 _ (wait',brk).
            (if brk then \<exists>a'. E a a' \<and> F a'
            else set wait' \<subseteq> set wait \<union> set l1 \<and> set l1 \<inter> Collect F = {}
              \<and> (\<forall> x \<in> set wait \<union> set l1. \<not> empty x \<longrightarrow> (\<exists> x' \<in> set wait'. x \<preceq> x')))
            \<and> (\<forall> x \<in> set wait'. \<not> empty x)"]
        )
            apply (auto; fail)
           apply (auto; fail)
          using succs_correct[of a] apply (auto; fail)
         using succs_correct[of a] apply (auto; fail)
        apply (auto; fail)
  subgoal
    apply (clarsimp split: if_split_asm)
     apply rule
      apply blast
     apply rule
      apply blast
     apply (meson empty_mono local.trans)
    apply rule
     apply blast
    apply (meson empty_mono local.trans)
    done
      apply (auto split: if_split_asm; fail)
     apply (auto; fail)
    apply (auto; fail)
  using succs_correct[of a] apply (auto; fail)
  apply (auto; fail)
  done

end

context Worklist2
begin

  lemma add_succ1'_ref[refine]:
    "add_succ1' wait a \<le> \<Down>(Id \<times>\<^sub>r bool_rel) (add_succ1 wait' a')"
    if "(wait,wait')\<in>Id" "(a,a')\<in>b_rel Id reachable" "\<forall> x \<in> set wait'. \<not> empty x"
    unfolding add_succ1'_def add_succ1_def
    using that
    apply (refine_vcg nfoldli_refine)
         apply refine_dref_type
         apply (auto simp: empty_subsumes' cong: filter_cong)
    by (metis empty_mono empty_subsumes' filter_True)+

  lemma add_succ1'_ref'[refine]:
    "add_succ1' wait a \<le> \<Down>(Id \<times>\<^sub>r bool_rel) (add_succ_spec_list wait' a')"
    if "(wait,wait')\<in>Id" "(a,a')\<in>b_rel Id reachable" "\<forall> x \<in> set wait'. \<not> empty x"
    using that
  proof -
    note add_succ1'_ref
    also note add_succ1_ref
    finally show ?thesis
      using that by - auto
  qed

  definition worklist_algo1' where
    "worklist_algo1' = do
      {
        if F a\<^sub>0 then RETURN True
        else do {
          let passed = {};
          let wait = [a\<^sub>0];
          (passed, wait, brk) \<leftarrow> WHILEIT worklist_inv_list (\<lambda> (passed, wait, brk). \<not> brk \<and> wait \<noteq> [])
            (\<lambda> (passed, wait, brk). do
              {
                (a, wait) \<leftarrow> take_from_list wait;
                if (\<exists> a' \<in> passed. a \<unlhd> a') then RETURN (passed, wait, brk) else
                do
                  {
                    (wait,brk) \<leftarrow> add_succ1' wait a;
                    let passed = insert a passed;
                    RETURN (passed, wait, brk)
                  }
              }
            )
            (passed, wait, False);
            RETURN brk
        }
      }
    "

  lemma take_from_list_ref[refine]:
    "take_from_list wait \<le>
     \<Down> {((x, wait), (y, wait')). x = y \<and> wait = wait' \<and> \<not> empty x \<and> (\<forall> a \<in> set wait. \<not> empty a)}
       (take_from_list wait')"
    if "wait = wait'" "\<forall> a \<in> set wait. \<not> empty a" "wait \<noteq> []"
    using that
    by (auto 4 4 simp: pw_le_iff refine_pw_simps dest!: take_from_list_correct)

  lemma worklist_algo1_list_ref[refine]: "worklist_algo1' \<le> \<Down>Id worklist_algo_list"
    unfolding worklist_algo1'_def worklist_algo_list_def
    apply (refine_rcg)
    apply refine_dref_type
    unfolding worklist_inv_list_def
    by auto

  definition worklist_algo1 where
    "worklist_algo1 \<equiv> if empty a\<^sub>0 then RETURN False else worklist_algo1'"

  lemma worklist_algo1_ref[refine]: "worklist_algo1 \<le> \<Down>Id worklist_algo''"
    unfolding worklist_algo1_def worklist_algo''_def
  proof clarsimp
    assume "\<not> empty a\<^sub>0"
    note worklist_algo1_list_ref
    also note worklist_algo_list_ref
    finally show "worklist_algo1' \<le> worklist_algo'" by simp
  qed

end \<comment> \<open>Worklist2\<close>

context Worklist3_Defs
begin

  definition
    "add_succ2 wait a \<equiv>
     nfoldli (succs a) (\<lambda>(_,brk). \<not>brk)
      (\<lambda>a (wait,brk).
        if empty a then RETURN (wait, False)
        else if F' a then RETURN (wait,True)
        else RETURN (
          if \<exists> x \<in> set wait. a \<unlhd> x \<and> \<not> x \<unlhd> a
          then [x \<leftarrow> wait. \<not> x \<unlhd> a]
          else a # [x \<leftarrow> wait. \<not> x \<unlhd> a],False)
      )
      (wait,False)"

  definition
    "filter_insert_wait wait a \<equiv>
     if \<exists> x \<in> set wait. a \<unlhd> x \<and> \<not> x \<unlhd> a
     then [x \<leftarrow> wait. \<not> x \<unlhd> a]
     else a # [x \<leftarrow> wait. \<not> x \<unlhd> a]"

end

context Worklist3
begin

  lemma filter_insert_wait_alt_def:
    "filter_insert_wait wait a = (
      let
         (f, xs) =
           fold (\<lambda> x (f, xs). if x \<unlhd> a then (f, xs) else (f \<or> a \<unlhd> x, x # xs)) wait (False, [])
       in
         if f then rev xs else a # rev xs
    )
    "
  proof -
    have
      "fold (\<lambda> x (f, xs). if x \<unlhd> a then (f, xs) else (f \<or> a \<unlhd> x, x # xs)) wait (f, xs)
     = (f \<or> (\<exists> x \<in> set wait. a \<unlhd> x \<and> \<not> x \<unlhd> a), rev [x \<leftarrow> wait. \<not> x \<unlhd> a] @ xs)" for f xs
      by (induction wait arbitrary: f xs; simp)
    then show ?thesis unfolding filter_insert_wait_def by auto
  qed

  lemma add_succ2_alt_def:
    "add_succ2 wait a \<equiv>
     nfoldli (succs a) (\<lambda>(_,brk). \<not>brk)
      (\<lambda>a (wait,brk).
        if empty a then RETURN (wait, False)
        else if F' a then RETURN (wait, True)
        else RETURN (filter_insert_wait wait a, False)
      )
      (wait,False)"
    unfolding add_succ2_def filter_insert_wait_def by (intro HOL.eq_reflection HOL.refl)

  lemma add_succ2_ref[refine]:
    "add_succ2 wait a \<le> \<Down>(Id \<times>\<^sub>r bool_rel) (add_succ1' wait' a')"
    if "(wait,wait')\<in>Id" "(a,a')\<in>Id"
    unfolding add_succ2_def add_succ1'_def
    apply (rule nfoldli_refine)
       apply refine_dref_type
    using that by (auto simp: F_split)

  definition worklist_algo2' where
    "worklist_algo2' = do
      {
        if F' a\<^sub>0 then RETURN True
        else do {
          let passed = {};
          let wait = [a\<^sub>0];
          (passed, wait, brk) \<leftarrow> WHILEIT worklist_inv_list (\<lambda> (passed, wait, brk). \<not> brk \<and> wait \<noteq> [])
            (\<lambda> (passed, wait, brk). do
              {
                (a, wait) \<leftarrow> take_from_list wait;
                if (\<exists> a' \<in> passed. a \<unlhd> a') then RETURN (passed, wait, brk) else
                do
                  {
                    (wait,brk) \<leftarrow> add_succ2 wait a;
                    let passed = insert a passed;
                    RETURN (passed, wait, brk)
                  }
              }
            )
            (passed, wait, False);
            RETURN brk
        }
      }
    "

  lemma worklist_algo2'_ref[refine]: "worklist_algo2' \<le> \<Down>Id worklist_algo1'" if "\<not> empty a\<^sub>0"
    unfolding worklist_algo2'_def worklist_algo1'_def
    using that
    supply take_from_list_ref [refine del]
    apply refine_rcg
              apply refine_dref_type
    by (auto simp: F_split)

  definition worklist_algo2 where
    "worklist_algo2 \<equiv> if empty a\<^sub>0 then RETURN False else worklist_algo2'"

  lemma worklist_algo2_ref[refine]: "worklist_algo2 \<le> \<Down>Id worklist_algo''"
  proof -
    have "worklist_algo2 \<le> \<Down>Id worklist_algo1"
      unfolding worklist_algo2_def worklist_algo1_def
      by refine_rcg standard
    also note worklist_algo1_ref
    finally show ?thesis .
  qed
end \<comment> \<open>Worklist3\<close>

end \<comment> \<open>Theory\<close>

author: wimmers

repo: munta

save_path: github-repos/isabelle/wimmers-munta


text:
theory Proof_2_36
  imports Proofs_2
begin

theorem proof_2_36: "VC36 inv2 env s0 userAtTop_value userAtBottom_value directionSwitch_value alarmButton_value stuck_value"
  apply(simp only: VC36_def inv2_def R2_def extraInv_def)
  apply(rule impI)
  apply(rule conjI)
   apply(rule conjI)
    apply simp
   apply((drule conjE)+)
                      prefer 22
                      apply assumption
                      prefer 21
                      apply assumption
                      prefer 20
                      apply assumption
                     prefer 19
                     apply assumption
                    prefer 18
                    apply assumption
                   prefer 17
                   apply assumption
                  prefer 16
                  apply assumption
                 prefer 15
                 apply assumption
                prefer 14
                apply assumption
               prefer 13
               apply assumption
              prefer 12
              apply assumption
             prefer 11
             apply assumption
            prefer 10
            apply assumption
           prefer 9
           apply assumption
          prefer 8
          apply assumption
         prefer 7
         apply assumption
        prefer 6
        apply assumption
       prefer 5
       apply assumption
      prefer 4
      apply assumption
     prefer 3
     apply assumption
    prefer 2
    apply assumption
   apply (metis getPstate.simps(9) substate_refl zero_neq_numeral)

author: ivchernenko


text:
theory Reg_Exp_Example
imports
  "HOL-Library.Predicate_Compile_Quickcheck"
  "HOL-Library.Code_Prolog"
begin

text \<open>An example from the experiments from SmallCheck (\<^url>\<open>https://www.cs.york.ac.uk/fp/smallcheck\<close>)\<close>
text \<open>The example (original in Haskell) was imported with Haskabelle and
  manually slightly adapted.
\<close>

datatype Nat = Zer
             | Suc Nat

fun sub :: "Nat \<Rightarrow> Nat \<Rightarrow> Nat"
where
  "sub x y = (case y of
                 Zer \<Rightarrow> x
               | Suc y' \<Rightarrow> case x of
                                         Zer \<Rightarrow> Zer
                                       | Suc x' \<Rightarrow> sub x' y')"

datatype Sym = N0
             | N1 Sym

datatype RE = Sym Sym
            | Or RE RE
            | Seq RE RE
            | And RE RE
            | Star RE
            | Empty

function accepts :: "RE \<Rightarrow> Sym list \<Rightarrow> bool" and
    seqSplit :: "RE \<Rightarrow> RE \<Rightarrow> Sym list \<Rightarrow> Sym list \<Rightarrow> bool" and
    seqSplit'' :: "RE \<Rightarrow> RE \<Rightarrow> Sym list \<Rightarrow> Sym list \<Rightarrow> bool" and
    seqSplit' :: "RE \<Rightarrow> RE \<Rightarrow> Sym list \<Rightarrow> Sym list \<Rightarrow> bool"
where
  "accepts re ss = (case re of
                       Sym n \<Rightarrow> case ss of
                                              Nil \<Rightarrow> False
                                            | (n' # ss') \<Rightarrow> n = n' & List.null ss'
                     | Or re1 re2 \<Rightarrow> accepts re1 ss | accepts re2 ss
                     | Seq re1 re2 \<Rightarrow> seqSplit re1 re2 Nil ss
                     | And re1 re2 \<Rightarrow> accepts re1 ss & accepts re2 ss
                     | Star re' \<Rightarrow> case ss of
                                                 Nil \<Rightarrow> True
                                               | (s # ss') \<Rightarrow> seqSplit re' re [s] ss'
                     | Empty \<Rightarrow> List.null ss)"
| "seqSplit re1 re2 ss2 ss = (seqSplit'' re1 re2 ss2 ss | seqSplit' re1 re2 ss2 ss)"
| "seqSplit'' re1 re2 ss2 ss = (accepts re1 ss2 & accepts re2 ss)"
| "seqSplit' re1 re2 ss2 ss = (case ss of
                                  Nil \<Rightarrow> False
                                | (n # ss') \<Rightarrow> seqSplit re1 re2 (ss2 @ [n]) ss')"
by pat_completeness auto

termination
  sorry

fun rep :: "Nat \<Rightarrow> RE \<Rightarrow> RE"
where
  "rep n re = (case n of
                  Zer \<Rightarrow> Empty
                | Suc n' \<Rightarrow> Seq re (rep n' re))"

fun repMax :: "Nat \<Rightarrow> RE \<Rightarrow> RE"
where
  "repMax n re = (case n of
                     Zer \<Rightarrow> Empty
                   | Suc n' \<Rightarrow> Or (rep n re) (repMax n' re))"

fun repInt' :: "Nat \<Rightarrow> Nat \<Rightarrow> RE \<Rightarrow> RE"
where
  "repInt' n k re = (case k of
                        Zer \<Rightarrow> rep n re
                      | Suc k' \<Rightarrow> Or (rep n re) (repInt' (Suc n) k' re))"

fun repInt :: "Nat \<Rightarrow> Nat \<Rightarrow> RE \<Rightarrow> RE"
where
  "repInt n k re = repInt' n (sub k n) re"

fun prop_regex :: "Nat * Nat * RE * RE * Sym list \<Rightarrow> bool"
where
  "prop_regex (n, (k, (p, (q, s)))) =
    ((accepts (repInt n k (And p q)) s) = (accepts (And (repInt n k p) (repInt n k q)) s))"

lemma "accepts (repInt n k (And p q)) s --> accepts (And (repInt n k p) (repInt n k q)) s"
(*nitpick
quickcheck[tester = random, iterations = 10000]
quickcheck[tester = predicate_compile_wo_ff]
quickcheck[tester = predicate_compile_ff_fs]*)
oops

setup \<open>
  Context.theory_map
    (Quickcheck.add_tester ("prolog", (Code_Prolog.active, Code_Prolog.test_goals)))
\<close>

setup \<open>Code_Prolog.map_code_options (K
  {ensure_groundness = true,
   limit_globally = NONE,
   limited_types = [(\<^typ>\<open>Sym\<close>, 0), (\<^typ>\<open>Sym list\<close>, 2), (\<^typ>\<open>RE\<close>, 6)],
   limited_predicates = [(["repIntPa"], 2), (["repP"], 2), (["subP"], 0),
    (["accepts", "acceptsaux", "seqSplit", "seqSplita", "seqSplitaux", "seqSplitb"], 25)],
   replacing =
     [(("repP", "limited_repP"), "lim_repIntPa"),
      (("subP", "limited_subP"), "repIntP"),
      (("repIntPa", "limited_repIntPa"), "repIntP"),
      (("accepts", "limited_accepts"), "quickcheck")],
   manual_reorder = []})\<close>

text \<open>Finding the counterexample still seems out of reach for the
 prolog-style generation.\<close>

lemma "accepts (And (repInt n k p) (repInt n k q)) s --> accepts (repInt n k (And p q)) s"
quickcheck[exhaustive]
quickcheck[tester = random, iterations = 1000]
(*quickcheck[tester = predicate_compile_wo_ff]*)
(*quickcheck[tester = predicate_compile_ff_fs, iterations = 1]*)
(*quickcheck[tester = prolog, iterations = 1, size = 1]*)
oops

section \<open>Given a partial solution\<close>

lemma
(*  assumes "n = Zer"
  assumes "k = Suc (Suc Zer)"*)
  assumes "p = Sym N0"
  assumes "q = Seq (Sym N0) (Sym N0)"
(*  assumes "s = [N0, N0]"*)
  shows "accepts (And (repInt n k p) (repInt n k q)) s --> accepts (repInt n k (And p q)) s"
(*quickcheck[tester = predicate_compile_wo_ff, iterations = 1]*)
quickcheck[tester = prolog, iterations = 1, size = 1]
oops

section \<open>Checking the counterexample\<close>

definition a_sol
where
  "a_sol = (Zer, (Suc (Suc Zer), (Sym N0, (Seq (Sym N0) (Sym N0), [N0, N0]))))"

lemma
  assumes "n = Zer"
  assumes "k = Suc (Suc Zer)"
  assumes "p = Sym N0"
  assumes "q = Seq (Sym N0) (Sym N0)"
  assumes "s = [N0, N0]"
  shows "accepts (repInt n k (And p q)) s --> accepts (And (repInt n k p) (repInt n k q)) s"
(*quickcheck[tester = predicate_compile_wo_ff]*)
oops

lemma
  assumes "n = Zer"
  assumes "k = Suc (Suc Zer)"
  assumes "p = Sym N0"
  assumes "q = Seq (Sym N0) (Sym N0)"
  assumes "s = [N0, N0]"
  shows "accepts (And (repInt n k p) (repInt n k q)) s --> accepts (repInt n k (And p q)) s"
(*quickcheck[tester = predicate_compile_wo_ff, iterations = 1, expect = counterexample]*)
quickcheck[tester = prolog, iterations = 1, size = 1]
oops

lemma
  assumes "n = Zer"
  assumes "k = Suc (Suc Zer)"
  assumes "p = Sym N0"
  assumes "q = Seq (Sym N0) (Sym N0)"
  assumes "s = [N0, N0]"
shows "prop_regex (n, (k, (p, (q, s))))"
quickcheck[tester = smart_exhaustive, depth = 30]
quickcheck[tester = prolog]
oops

lemma "prop_regex a_sol"
quickcheck[tester = random]
quickcheck[tester = smart_exhaustive]
oops

value "prop_regex a_sol"

end

repo: isabelle