text:
(*  Title:      HOL/Bali/AxExample.thy
    Author:     David von Oheimb
*)

subsection {* Example of a proof based on the Bali axiomatic semantics *}

theory AxExample
imports AxSem Example
begin

definition
  arr_inv :: "st \<Rightarrow> bool" where
 "arr_inv = (\<lambda>s. \<exists>obj a T el. globs s (Stat Base) = Some obj \<and>
                              values obj (Inl (arr, Base)) = Some (Addr a) \<and>
                              heap s a = Some \<lparr>tag=Arr T 2,values=el\<rparr>)"

lemma arr_inv_new_obj:
"\<And>a. \<lbrakk>arr_inv s; new_Addr (heap s)=Some a\<rbrakk> \<Longrightarrow> arr_inv (gupd(Inl a\<mapsto>x) s)"
apply (unfold arr_inv_def)
apply (force dest!: new_AddrD2)
done

lemma arr_inv_set_locals [simp]: "arr_inv (set_locals l s) = arr_inv s"
apply (unfold arr_inv_def)
apply (simp (no_asm))
done

lemma arr_inv_gupd_Stat [simp]:
  "Base \<noteq> C \<Longrightarrow> arr_inv (gupd(Stat C\<mapsto>obj) s) = arr_inv s"
apply (unfold arr_inv_def)
apply (simp (no_asm_simp))
done

lemma ax_inv_lupd [simp]: "arr_inv (lupd(x\<mapsto>y) s) = arr_inv s"
apply (unfold arr_inv_def)
apply (simp (no_asm))
done

declare split_if_asm [split del]
declare lvar_def [simp]

ML {*
fun inst1_tac ctxt s t xs st =
  (case AList.lookup (op =) (rev (Term.add_var_names (Thm.prop_of st) [])) s of
    SOME i => Rule_Insts.instantiate_tac ctxt [((s, i), t)] xs st
  | NONE => Seq.empty);

val ax_tac =
  REPEAT o rtac allI THEN'
  resolve_tac (@{thm ax_Skip} :: @{thm ax_StatRef} :: @{thm ax_MethdN} :: @{thm ax_Alloc} ::
    @{thm ax_Alloc_Arr} :: @{thm ax_SXAlloc_Normal} :: @{thms ax_derivs.intros(8-)});
*}

theorem ax_test: "tprg,({}::'a triple set)\<turnstile>
  {Normal (\<lambda>Y s Z::'a. heap_free four s \<and> \<not>initd Base s \<and> \<not> initd Ext s)}
  .test [Class Base].
  {\<lambda>Y s Z. abrupt s = Some (Xcpt (Std IndOutBound))}"
apply (unfold test_def arr_viewed_from_def)
apply (tactic "ax_tac 1" (*;;*))
defer (* We begin with the last assertion, to synthesise the intermediate
         assertions, like in the fashion of the weakest
         precondition. *)
apply  (tactic "ax_tac 1" (* Try *))
defer
apply    (tactic {* inst1_tac @{context} "Q"
                 "\<lambda>Y s Z. arr_inv (snd s) \<and> tprg,s\<turnstile>catch SXcpt NullPointer" [] *})
prefer 2
apply    simp
apply   (rule_tac P' = "Normal (\<lambda>Y s Z. arr_inv (snd s))" in conseq1)
prefer 2
apply    clarsimp
apply   (rule_tac Q' = "(\<lambda>Y s Z. ?Q Y s Z)\<leftarrow>=False\<down>=\<diamondsuit>" in conseq2)
prefer 2
apply    simp
apply   (tactic "ax_tac 1" (* While *))
prefer 2
apply    (rule ax_impossible [THEN conseq1], clarsimp)
apply   (rule_tac P' = "Normal ?P" in conseq1)
prefer 2
apply    clarsimp
apply   (tactic "ax_tac 1")
apply   (tactic "ax_tac 1" (* AVar *))
prefer 2
apply    (rule ax_subst_Val_allI)
apply    (tactic {* inst1_tac @{context} "P'" "\<lambda>a. Normal (PP a\<leftarrow>x)" ["PP", "x"] *})
apply    (simp del: avar_def2 peek_and_def2)
apply    (tactic "ax_tac 1")
apply   (tactic "ax_tac 1")
      (* just for clarification: *)
apply   (rule_tac Q' = "Normal (\<lambda>Var:(v, f) u ua. fst (snd (avar tprg (Intg 2) v u)) = Some (Xcpt (Std IndOutBound)))" in conseq2)
prefer 2
apply    (clarsimp simp add: split_beta)
apply   (tactic "ax_tac 1" (* FVar *))
apply    (tactic "ax_tac 2" (* StatRef *))
apply   (rule ax_derivs.Done [THEN conseq1])
apply   (clarsimp simp add: arr_inv_def inited_def in_bounds_def)
defer
apply  (rule ax_SXAlloc_catch_SXcpt)
apply  (rule_tac Q' = "(\<lambda>Y (x, s) Z. x = Some (Xcpt (Std NullPointer)) \<and> arr_inv s) \<and>. heap_free two" in conseq2)
prefer 2
apply   (simp add: arr_inv_new_obj)
apply  (tactic "ax_tac 1")
apply  (rule_tac C = "Ext" in ax_Call_known_DynT)
apply     (unfold DynT_prop_def)
apply     (simp (no_asm))
apply    (intro strip)
apply    (rule_tac P' = "Normal ?P" in conseq1)
apply     (tactic "ax_tac 1" (* Methd *))
apply     (rule ax_thin [OF _ empty_subsetI])
apply     (simp (no_asm) add: body_def2)
apply     (tactic "ax_tac 1" (* Body *))
(* apply       (rule_tac [2] ax_derivs.Abrupt) *)
defer
apply      (simp (no_asm))
apply      (tactic "ax_tac 1") (* Comp *)
            (* The first statement in the  composition
                 ((Ext)z).vee = 1; Return Null
                will throw an exception (since z is null). So we can handle
                Return Null with the Abrupt rule *)
apply       (rule_tac [2] ax_derivs.Abrupt)

apply      (rule ax_derivs.Expr) (* Expr *)
apply      (tactic "ax_tac 1") (* Ass *)
prefer 2
apply       (rule ax_subst_Var_allI)
apply       (tactic {* inst1_tac @{context} "P'" "\<lambda>a vs l vf. PP a vs l vf\<leftarrow>x \<and>. p" ["PP", "x", "p"] *})
apply       (rule allI)
apply       (tactic {* simp_tac (@{context} delloop "split_all_tac" delsimps [@{thm peek_and_def2}, @{thm heap_def2}, @{thm subst_res_def2}, @{thm normal_def2}]) 1 *})
apply       (rule ax_derivs.Abrupt)
apply      (simp (no_asm))
apply      (tactic "ax_tac 1" (* FVar *))
apply       (tactic "ax_tac 2", tactic "ax_tac 2", tactic "ax_tac 2")
apply      (tactic "ax_tac 1")
apply     (tactic {* inst1_tac @{context} "R" "\<lambda>a'. Normal ((\<lambda>Vals:vs (x, s) Z. arr_inv s \<and> inited Ext (globs s) \<and> a' \<noteq> Null \<and> vs = [Null]) \<and>. heap_free two)" [] *})
apply     fastforce
prefer 4
apply    (rule ax_derivs.Done [THEN conseq1],force)
apply   (rule ax_subst_Val_allI)
apply   (tactic {* inst1_tac @{context} "P'" "\<lambda>a. Normal (PP a\<leftarrow>x)" ["PP", "x"] *})
apply   (simp (no_asm) del: peek_and_def2 heap_free_def2 normal_def2 o_apply)
apply   (tactic "ax_tac 1")
prefer 2
apply   (rule ax_subst_Val_allI)
apply    (tactic {* inst1_tac @{context} "P'" "\<lambda>aa v. Normal (QQ aa v\<leftarrow>y)" ["QQ", "y"] *})
apply    (simp del: peek_and_def2 heap_free_def2 normal_def2)
apply    (tactic "ax_tac 1")
apply   (tactic "ax_tac 1")
apply  (tactic "ax_tac 1")
apply  (tactic "ax_tac 1")
(* end method call *)
apply (simp (no_asm))
    (* just for clarification: *)
apply (rule_tac Q' = "Normal ((\<lambda>Y (x, s) Z. arr_inv s \<and> (\<exists>a. the (locals s (VName e)) = Addr a \<and> obj_class (the (globs s (Inl a))) = Ext \<and>
 invocation_declclass tprg IntVir s (the (locals s (VName e))) (ClassT Base)
     \<lparr>name = foo, parTs = [Class Base]\<rparr> = Ext)) \<and>. initd Ext \<and>. heap_free two)"
  in conseq2)
prefer 2
apply  clarsimp
apply (tactic "ax_tac 1")
apply (tactic "ax_tac 1")
defer
apply  (rule ax_subst_Var_allI)
apply  (tactic {* inst1_tac @{context} "P'" "\<lambda>vf. Normal (PP vf \<and>. p)" ["PP", "p"] *})
apply  (simp (no_asm) del: split_paired_All peek_and_def2 initd_def2 heap_free_def2 normal_def2)
apply  (tactic "ax_tac 1" (* NewC *))
apply  (tactic "ax_tac 1" (* ax_Alloc *))
     (* just for clarification: *)
apply  (rule_tac Q' = "Normal ((\<lambda>Y s Z. arr_inv (store s) \<and> vf=lvar (VName e) (store s)) \<and>. heap_free three \<and>. initd Ext)" in conseq2)
prefer 2
apply   (simp add: invocation_declclass_def dynmethd_def)
apply   (unfold dynlookup_def)
apply   (simp add: dynmethd_Ext_foo)
apply   (force elim!: arr_inv_new_obj atleast_free_SucD atleast_free_weaken)
     (* begin init *)
apply  (rule ax_InitS)
apply     force
apply    (simp (no_asm))
apply   (tactic {* simp_tac (@{context} delloop "split_all_tac") 1 *})
apply   (rule ax_Init_Skip_lemma)
apply  (tactic {* simp_tac (@{context} delloop "split_all_tac") 1 *})
apply  (rule ax_InitS [THEN conseq1] (* init Base *))
apply      force
apply     (simp (no_asm))
apply    (unfold arr_viewed_from_def)
apply    (rule allI)
apply    (rule_tac P' = "Normal ?P" in conseq1)
apply     (tactic {* simp_tac (@{context} delloop "split_all_tac") 1 *})
apply     (tactic "ax_tac 1")
apply     (tactic "ax_tac 1")
apply     (rule_tac [2] ax_subst_Var_allI)
apply      (tactic {* inst1_tac @{context} "P'" "\<lambda>vf l vfa. Normal (P vf l vfa)" ["P"] *})
apply     (tactic {* simp_tac (@{context} delloop "split_all_tac" delsimps [@{thm split_paired_All}, @{thm peek_and_def2}, @{thm heap_free_def2}, @{thm initd_def2}, @{thm normal_def2}, @{thm supd_lupd}]) 2 *})
apply      (tactic "ax_tac 2" (* NewA *))
apply       (tactic "ax_tac 3" (* ax_Alloc_Arr *))
apply       (tactic "ax_tac 3")
apply      (tactic {* inst1_tac @{context} "P" "\<lambda>vf l vfa. Normal (P vf l vfa\<leftarrow>\<diamondsuit>)" ["P"] *})
apply      (tactic {* simp_tac (@{context} delloop "split_all_tac") 2 *})
apply      (tactic "ax_tac 2")
apply     (tactic "ax_tac 1" (* FVar *))
apply      (tactic "ax_tac 2" (* StatRef *))
apply     (rule ax_derivs.Done [THEN conseq1])
apply     (tactic {* inst1_tac @{context} "Q" "\<lambda>vf. Normal ((\<lambda>Y s Z. vf=lvar (VName e) (snd s)) \<and>. heap_free four \<and>. initd Base \<and>. initd Ext)" [] *})
apply     (clarsimp split del: split_if)
apply     (frule atleast_free_weaken [THEN atleast_free_weaken])
apply     (drule initedD)
apply     (clarsimp elim!: atleast_free_SucD simp add: arr_inv_def)
apply    force
apply   (tactic {* simp_tac (@{context} delloop "split_all_tac") 1 *})
apply   (rule ax_triv_Init_Object [THEN peek_and_forget2, THEN conseq1])
apply     (rule wf_tprg)
apply    clarsimp
apply   (tactic {* inst1_tac @{context} "P" "\<lambda>vf. Normal ((\<lambda>Y s Z. vf = lvar (VName e) (snd s)) \<and>. heap_free four \<and>. initd Ext)" [] *})
apply   clarsimp
apply  (tactic {* inst1_tac @{context} "PP" "\<lambda>vf. Normal ((\<lambda>Y s Z. vf = lvar (VName e) (snd s)) \<and>. heap_free four \<and>. Not \<circ> initd Base)" [] *})
apply  clarsimp
     (* end init *)
apply (rule conseq1)
apply (tactic "ax_tac 1")
apply clarsimp
done

(*
while (true) {
  if (i) {throw xcpt;}
  else i=j
}
*)
lemma Loop_Xcpt_benchmark:
 "Q = (\<lambda>Y (x,s) Z. x \<noteq> None \<longrightarrow> the_Bool (the (locals s i))) \<Longrightarrow>
  G,({}::'a triple set)\<turnstile>{Normal (\<lambda>Y s Z::'a. True)}
  .lab1\<bullet> While(Lit (Bool True)) (If(Acc (LVar i)) (Throw (Acc (LVar xcpt))) Else
        (Expr (Ass (LVar i) (Acc (LVar j))))). {Q}"
apply (rule_tac P' = "Q" and Q' = "Q\<leftarrow>=False\<down>=\<diamondsuit>" in conseq12)
apply  safe
apply  (tactic "ax_tac 1" (* Loop *))
apply   (rule ax_Normal_cases)
prefer 2
apply    (rule ax_derivs.Abrupt [THEN conseq1], clarsimp simp add: Let_def)
apply   (rule conseq1)
apply    (tactic "ax_tac 1")
apply   clarsimp
prefer 2
apply  clarsimp
apply (tactic "ax_tac 1" (* If *))
apply  (tactic
  {* inst1_tac @{context} "P'" "Normal (\<lambda>s.. (\<lambda>Y s Z. True)\<down>=Val (the (locals s i)))" [] *})
apply  (tactic "ax_tac 1")
apply  (rule conseq1)
apply   (tactic "ax_tac 1")
apply  clarsimp
apply (rule allI)
apply (rule ax_escape)
apply auto
apply  (rule conseq1)
apply   (tactic "ax_tac 1" (* Throw *))
apply   (tactic "ax_tac 1")
apply   (tactic "ax_tac 1")
apply  clarsimp
apply (rule_tac Q' = "Normal (\<lambda>Y s Z. True)" in conseq2)
prefer 2
apply  clarsimp
apply (rule conseq1)
apply  (tactic "ax_tac 1")
apply  (tactic "ax_tac 1")
prefer 2
apply   (rule ax_subst_Var_allI)
apply   (tactic {* inst1_tac @{context} "P'" "\<lambda>b Y ba Z vf. \<lambda>Y (x,s) Z. x=None \<and> snd vf = snd (lvar i s)" [] *})
apply   (rule allI)
apply   (rule_tac P' = "Normal ?P" in conseq1)
prefer 2
apply    clarsimp
apply   (tactic "ax_tac 1")
apply   (rule conseq1)
apply    (tactic "ax_tac 1")
apply   clarsimp
apply  (tactic "ax_tac 1")
apply clarsimp
done

end

author: Josh-Tilles

repo: isabelle


text:
           (*-------------------------------------------*
            |    Example 1 [Roscoe_Dathi_1987 P.10]     |
            |             WITH computation              |
            |  Self-timed version of a systolic array   |
            |                   June 2005               |
            |               December 2005  (modified)   |
            |                                           |
            |   on DFP on CSP-Prover ver.3.0            |
            |              September 2006  (modified)   |
            |                                           |
            |   on DFP on CSP-Prover ver.4.0            |
            |                  April 2007  (modified)   |
            |        Yoshinao Isobe (AIST JAPAN)        |
            *-------------------------------------------*)

theory SA_local
imports SA_definition
begin

(*----------------------*
 |     small lemma      |
 *----------------------*)

lemma possible_pairs:
    "{ (peF ij, Alpha_pe ij) | ij:{(i1, j1), (i2, j2)} }Fnet >>
       (i1, j1) --[(t, Yf), Lambda]-->o (i2, j2)
     ==> (i1 = i2 & j1 = Suc j2)
       | (i1 = i2 & j2 = Suc j1)
       | (i1 = Suc i2 & j1 = j2)
       | (i2 = Suc i1 & j1 = j2)"
apply (simp add: isUngrantedRequestOfwrt_def)
apply (simp add: isUngrantedRequestOf_def)
apply (simp add: isRequestOf_def)
apply (simp add: isStateOf_def)
apply (simp add: Alpha_pe.simps)
apply (auto)
done

(*--------------------------------*
 |       local calculation        |
 *--------------------------------*)

(*** i j hori ***)

lemma local_i_j_hori_ALL:
   "ALL s. ((s, Yf (i, j)) : peF_rec n (i, j) &
            (EX x. Ev (hori (i,Suc j) x) ~: Yf (i,j)))
    --> Suc (Suc (4 * lengtht (s rest-tr (range(hori (i, Suc j)))))) <= lengtht s"
apply (induct_tac n)
apply (simp)

apply (intro allI impI)
apply (simp add: Faiures_in_def)
apply (elim disjE conjE exE, simp_all add: image_iff)

apply (simp add: Faiures_in_hori_def)
apply (elim disjE conjE exE, simp_all add: image_iff)

apply (simp add: Faiures_out_def)
apply (elim disjE conjE exE, simp_all add: image_iff)
apply (simp add: Faiures_out_hori_def)
apply (elim disjE conjE exE, simp_all add: image_iff)

apply (simp add: Faiures_out_vert_def)
apply (elim disjE conjE exE, simp_all add: image_iff)

apply (simp add: Faiures_in_vert_def)
apply (elim disjE conjE exE, simp_all add: image_iff)

apply (simp add: Faiures_out_def)
apply (elim disjE conjE exE, simp_all add: image_iff)
apply (simp add: Faiures_out_hori_def)
apply (elim disjE conjE exE, simp_all add: image_iff)

apply (simp add: Faiures_out_vert_def)
apply (elim disjE conjE exE, simp_all add: image_iff)
done

lemma local_i_j_hori:
   "[| (s, Yf (i, j)) : peF (i, j) ;
       EX x. Ev (hori (i, Suc j) x) ~: Yf (i, j) |]
    ==> Suc (Suc (4 * lengtht (s rest-tr (range (hori (i, Suc j)))))) <= lengtht s"
apply (simp add: peF_def)
apply (elim conjE exE, simp)
apply (insert local_i_j_hori_ALL[of Yf i j])
by (auto)

(*** i (Suc j) hori ***)

lemma local_i_Suc_j_hori_ALL:
   "ALL s. ((s, Yf (i, Suc j)) : peF_rec n (i, Suc j) &
       (ALL x. Ev (hori (i,Suc j) x) : Yf (i,Suc j)))
    --> Suc (lengtht s) <= 4 * lengtht (s rest-tr (range (hori (i, Suc j))))"
apply (induct_tac n)
apply (simp)

apply (intro allI impI)
apply (simp add: Faiures_in_def)
apply (elim disjE conjE exE, simp_all add: image_iff)

apply (simp add: Faiures_in_hori_def)
apply (elim disjE conjE exE, simp_all add: image_iff)

apply (simp add: Faiures_out_def)
apply (elim disjE conjE exE, simp_all add: image_iff)
apply (simp add: Faiures_out_hori_def)
apply (elim disjE conjE exE, simp_all add: image_iff)

apply (simp add: Faiures_out_vert_def)
apply (elim disjE conjE exE, simp_all add: image_iff)

apply (simp add: Faiures_in_vert_def)
apply (elim disjE conjE exE, simp_all add: image_iff)

apply (simp add: Faiures_out_def)
apply (elim disjE conjE exE, simp_all add: image_iff)
apply (simp add: Faiures_out_hori_def)
apply (elim disjE conjE exE, simp_all add: image_iff)

apply (simp add: Faiures_out_vert_def)
apply (elim disjE conjE exE, simp_all add: image_iff)
done

lemma local_i_Suc_j_hori:
   "[| (s, Yf (i, Suc j)) : peF (i, Suc j) ;
       ALL x. Ev (hori (i,Suc j) x) : Yf (i,Suc j) |]
    ==> Suc (lengtht s) <= 4 * lengtht (s rest-tr (range (hori (i, Suc j))))"
apply (simp add: peF_def)
apply (elim conjE exE, simp)
apply (insert local_i_Suc_j_hori_ALL[of Yf i j])
by (simp)

(*** i j vert ***)

lemma local_i_j_vert_ALL:
   "ALL s. ((s, Yf (i, j)) : peF_rec n (i, j) &
            (EX x. Ev (vert (Suc i, j) x) ~: Yf (i,j)))
    --> Suc (Suc (4 * lengtht (s rest-tr (range(vert (Suc i, j)))))) <= lengtht s"
apply (induct_tac n)
apply (simp)

apply (intro allI impI)
apply (simp add: Faiures_in_def)
apply (elim disjE conjE exE, simp_all add: image_iff)

apply (simp add: Faiures_in_hori_def)
apply (elim disjE conjE exE, simp_all add: image_iff)

apply (simp add: Faiures_out_def)
apply (elim disjE conjE exE, simp_all add: image_iff)
apply (simp add: Faiures_out_hori_def)
apply (elim disjE conjE exE, simp_all add: image_iff)

apply (simp add: Faiures_out_vert_def)
apply (elim disjE conjE exE, simp_all add: image_iff)

apply (simp add: Faiures_in_vert_def)
apply (elim disjE conjE exE, simp_all add: image_iff)

apply (simp add: Faiures_out_def)
apply (elim disjE conjE exE, simp_all add: image_iff)
apply (simp add: Faiures_out_hori_def)
apply (elim disjE conjE exE, simp_all add: image_iff)

apply (simp add: Faiures_out_vert_def)
apply (elim disjE conjE exE, simp_all add: image_iff)
done

lemma local_i_j_vert:
   "[| (s, Yf (i, j)) : peF (i, j) ; EX x. Ev (vert (Suc i, j) x) ~: Yf (i,j) |]
    ==> Suc (Suc (4 * lengtht (s rest-tr (range (vert (Suc i, j)))))) <= lengtht s"
apply (simp add: peF_def)
apply (elim conjE exE, simp)
apply (insert local_i_j_vert_ALL[of Yf i j])
by (auto)

(*** (Suc i) j vert ***)

lemma local_Suc_i_j_vert_ALL:
   "ALL s. ((s, Yf (Suc i, j)) : peF_rec n (Suc i, j) &
            (ALL x. Ev (vert (Suc i, j) x) : Yf (Suc i, j)))
    --> Suc (lengtht s) <= 4 * lengtht (s rest-tr (range (vert (Suc i, j))))"
apply (induct_tac n)
apply (simp)

apply (intro allI impI)
apply (simp add: Faiures_in_def)
apply (elim disjE conjE exE, simp_all add: image_iff)

apply (simp add: Faiures_in_hori_def)
apply (elim disjE conjE exE, simp_all add: image_iff)

apply (simp add: Faiures_out_def)
apply (elim disjE conjE exE, simp_all add: image_iff)
apply (simp add: Faiures_out_hori_def)
apply (elim disjE conjE exE, simp_all add: image_iff)

apply (simp add: Faiures_out_vert_def)
apply (elim disjE conjE exE, simp_all add: image_iff)

apply (simp add: Faiures_in_vert_def)
apply (elim disjE conjE exE, simp_all add: image_iff)

apply (simp add: Faiures_out_def)
apply (elim disjE conjE exE, simp_all add: image_iff)
apply (simp add: Faiures_out_hori_def)
apply (elim disjE conjE exE, simp_all add: image_iff)

apply (simp add: Faiures_out_vert_def)
apply (elim disjE conjE exE, simp_all add: image_iff)
done

lemma local_Suc_i_j_vert:
   "[| (s, Yf (Suc i, j)) : peF (Suc i, j) ;
       ALL x. Ev (vert (Suc i, j) x) : Yf (Suc i, j) |]
    ==> Suc (lengtht s) <= 4 * lengtht (s rest-tr (range (vert (Suc i, j))))"
apply (simp add: peF_def)
apply (elim conjE exE, simp)
apply (insert local_Suc_i_j_vert_ALL[of Yf i j])
by (simp)

(****** reverse ******)

(*** i j hori ***)

lemma local_i_j_hori_rev_ALL:
   "ALL s. ((s, Yf (i, j)) : peF_rec n (i, j) &
            (ALL x. Ev (hori (i,Suc j) x) : Yf (i,j)))
    -->  lengtht s <= (Suc (4 * lengtht (s rest-tr (range (hori (i, Suc j))))))"
apply (induct_tac n)
apply (simp)

apply (intro allI impI)
apply (simp add: Faiures_in_def)
apply (elim disjE conjE exE, simp_all add: image_iff)

apply (simp add: Faiures_in_hori_def)
apply (elim disjE conjE exE, simp_all add: image_iff)
apply (simp add: Faiures_out_def)
apply (elim disjE conjE exE)
apply (force)
apply (simp add: Faiures_out_hori_def)
apply (force)
apply (simp add: Faiures_out_vert_def)
apply (force)

apply (simp add: Faiures_in_vert_def)
apply (elim disjE conjE exE, simp_all add: image_iff)
apply (simp add: Faiures_out_def)
apply (elim disjE conjE exE)
apply (force)
apply (simp add: Faiures_out_hori_def)
apply (force)
apply (simp add: Faiures_out_vert_def)
apply (force)
done

lemma local_i_j_hori_rev:
   "[| (s, Yf (i, j)) : peF (i, j) ;
       ALL x. Ev (hori (i,Suc j) x) : Yf (i,j) |]
    ==> lengtht s <= (Suc (4 * lengtht (s rest-tr (range (hori (i, Suc j))))))"
apply (simp add: peF_def)
apply (elim conjE exE, simp)
apply (insert local_i_j_hori_rev_ALL[of Yf i j])
by (simp)

(*** i (Suc j) hori ***)

lemma local_i_Suc_j_hori_rev_ALL:
   "ALL s. ((s, Yf (i, Suc j)) : peF_rec n (i, Suc j) &
            (EX x. Ev (hori (i,Suc j) x) ~: Yf (i,Suc j)))
    --> 4 * lengtht (s rest-tr (range (hori (i, Suc j)))) <= lengtht s"
apply (induct_tac n)
apply (simp)

apply (intro allI impI)
apply (simp add: Faiures_in_def)
apply (elim disjE conjE exE, simp_all add: image_iff)

apply (simp add: Faiures_in_hori_def)
apply (elim disjE conjE exE, simp_all add: image_iff)

apply (simp add: Faiures_out_def)
apply (elim disjE conjE exE, simp_all add: image_iff)
apply (simp add: Faiures_out_hori_def)
apply (elim disjE conjE exE, simp_all add: image_iff)
apply (simp add: Faiures_out_vert_def)
apply (elim disjE conjE exE, simp_all add: image_iff)

apply (simp add: Faiures_in_vert_def)
apply (elim disjE conjE exE, simp_all add: image_iff)

apply (simp add: Faiures_out_def)
apply (elim disjE conjE exE, simp_all add: image_iff)
apply (simp add: Faiures_out_hori_def)
apply (elim disjE conjE exE, simp_all add: image_iff)
apply (simp add: Faiures_out_vert_def)
apply (elim disjE conjE exE, simp_all add: image_iff)
done

lemma local_i_Suc_j_hori_rev:
   "[| (s, Yf (i, Suc j)) : peF (i, Suc j) ;
       EX x. Ev (hori (i,Suc j) x) ~: Yf (i,Suc j) |]
    ==> 4 * lengtht (s rest-tr (range (hori (i, Suc j)))) <= lengtht s"
apply (simp add: peF_def)
apply (elim conjE exE, simp)
apply (insert local_i_Suc_j_hori_rev_ALL[of Yf i j])
by (auto)

(*** i j vert ***)

lemma local_i_j_vert_rev_ALL:
   "ALL s. ((s, Yf (i, j)) : peF_rec n (i, j) &
           (ALL x. Ev (vert (Suc i, j) x) : Yf (i,j)))
    -->  lengtht s <= (Suc (4 * lengtht (s rest-tr (range (vert (Suc i, j))))))"
apply (induct_tac n)
apply (simp)

apply (intro allI impI)
apply (simp add: Faiures_in_def)
apply (elim disjE conjE exE, simp_all add: image_iff)

apply (simp add: Faiures_in_hori_def)
apply (elim disjE conjE exE, simp_all add: image_iff)
apply (simp add: Faiures_out_def)
apply (elim disjE conjE exE)
apply (force)
apply (simp add: Faiures_out_hori_def)
apply (force)
apply (simp add: Faiures_out_vert_def)
apply (force)

apply (simp add: Faiures_in_vert_def)
apply (elim disjE conjE exE, simp_all add: image_iff)
apply (simp add: Faiures_out_def)
apply (elim disjE conjE exE)
apply (force)
apply (simp add: Faiures_out_hori_def)
apply (force)
apply (simp add: Faiures_out_vert_def)
apply (force)
done

lemma local_i_j_vert_rev:
   "[| (s, Yf (i, j)) : peF (i, j) ; ALL x. Ev (vert (Suc i, j) x) : Yf (i,j) |]
    ==> lengtht s <= (Suc (4 * lengtht (s rest-tr (range (vert (Suc i, j))))))"
apply (simp add: peF_def)
apply (elim conjE exE, simp)
apply (insert local_i_j_vert_rev_ALL[of Yf i j])
by (simp)

(*** (Suc i) j vert ***)

lemma local_Suc_i_j_vert_rev_ALL:
   "ALL s. ((s, Yf (Suc i, j)) : peF_rec n (Suc i, j) &
            (EX x. Ev (vert (Suc i, j) x) ~: Yf (Suc i, j)))
    --> 4 * lengtht (s rest-tr (range (vert (Suc i, j)))) <= lengtht s"
apply (induct_tac n)
apply (simp)

apply (intro allI impI)
apply (simp add: Faiures_in_def)
apply (elim disjE conjE exE, simp_all add: image_iff)

apply (simp add: Faiures_in_hori_def)
apply (elim disjE conjE exE, simp_all add: image_iff)

apply (simp add: Faiures_out_def)
apply (elim disjE conjE exE, simp_all add: image_iff)
apply (simp add: Faiures_out_hori_def)
apply (elim disjE conjE exE, simp_all add: image_iff)
apply (simp add: Faiures_out_vert_def)
apply (elim disjE conjE exE, simp_all add: image_iff)

apply (simp add: Faiures_in_vert_def)
apply (elim disjE conjE exE, simp_all add: image_iff)

apply (simp add: Faiures_out_def)
apply (elim disjE conjE exE, simp_all add: image_iff)
apply (simp add: Faiures_out_hori_def)
apply (elim disjE conjE exE, simp_all add: image_iff)
apply (simp add: Faiures_out_vert_def)
apply (elim disjE conjE exE, simp_all add: image_iff)
done

lemma local_Suc_i_j_vert_rev:
   "[| (s, Yf (Suc i, j)) : peF (Suc i, j) ;
       EX x. Ev (vert (Suc i, j) x) ~: Yf (Suc i, j) |]
    ==> 4 * lengtht (s rest-tr (range (vert (Suc i, j)))) <= lengtht s"
apply (simp add: peF_def)
apply (elim conjE exE, simp)
apply (insert local_Suc_i_j_vert_rev_ALL[of Yf i j])
by (auto)

(*---------------------------------------*
 |  ungranted request --> Yf properties  |
 *---------------------------------------*)

(* hori *)

lemma EX1_request_hori:
  "(Ev ` Alpha_pe (i, j) - Yf (i, j)) Int Ev ` Alpha_pe (i, Suc j) ~= {}
   ==> EX x. Ev (hori (i, Suc j) x) ~: Yf (i, j)"
by (auto simp add: Alpha_pe.simps)

lemma EX1_ungranted_hori_lm1:
  "[| (Ev ` Alpha_pe (i, j) - Yf (i, j)) Int Ev ` Alpha_pe (i, Suc j) ~= {} ;
       Ev ` Alpha_pe (i, j) Int Ev ` Alpha_pe (i, Suc j) <= Yf (i, j) Un Yf (i, Suc j) |]
   ==> EX x. Ev (hori (i, Suc j) x) : Yf (i, Suc j)"
by (auto simp add: Alpha_pe.simps)

lemma EX1_ungranted_hori_lm2:
  "ALL n x. (Ev (hori (i, Suc j) x) : Yf (i, Suc j) &
    (EX t. (t , Yf (i, Suc j)) : peF_rec n (i, Suc j)))
   --> (ALL x. Ev (hori (i, Suc j) x) : Yf (i, Suc j))"
apply (intro allI)
apply (induct_tac n)
apply (simp)
apply (intro allI impI)

apply (simp)
apply (simp add: Faiures_in_def)
apply (elim conjE exE disjE)
apply (force)                            (* contra *)

 (* hori *)
 apply (simp add: Faiures_in_hori_def)
 apply (elim conjE exE disjE)
 apply (force)                            (* contra *)
 apply (simp add: Faiures_out_def)
 apply (elim conjE exE disjE)
 apply (force)                            (* okay *)

  apply (simp add: Faiures_out_hori_def)
  apply (elim conjE exE disjE)
  apply (force)                            (* okay *)
  apply (force)                            (* induction *)

  apply (simp add: Faiures_out_vert_def)
  apply (elim conjE exE disjE)
  apply (force)                            (* okay *)
  apply (force)                            (* induction *)

 (* vert *)
 apply (simp add: Faiures_in_vert_def)
 apply (elim conjE exE disjE)
 apply (force)                            (* contra *)
 apply (simp add: Faiures_out_def)
 apply (elim conjE exE disjE)
 apply (force)                            (* okay *)

  apply (simp add: Faiures_out_hori_def)
  apply (elim conjE exE disjE)
  apply (force)                            (* okay *)
  apply (force)                            (* induction *)

  apply (simp add: Faiures_out_vert_def)
  apply (elim conjE exE disjE)
  apply (force)                            (* okay *)
  apply (force)                            (* induction *)
done

lemma EX1_ungranted_hori:
  "[| (Ev ` Alpha_pe (i, j) - Yf (i, j)) Int Ev ` Alpha_pe (i, Suc j) ~= {} ;
       Ev ` Alpha_pe (i, j) Int Ev ` Alpha_pe (i, Suc j) <= Yf (i, j) Un Yf (i, Suc j) ;
       (t , Yf (i, Suc j)) : peF (i, Suc j) |]
   ==> (ALL x. Ev (hori (i, Suc j) x) : Yf (i, Suc j))"
apply (insert EX1_ungranted_hori_lm1[of i j Yf])
apply (simp add: peF_def)
apply (elim conjE exE)
apply (simp)
apply (insert EX1_ungranted_hori_lm2[of i j Yf])
apply (drule_tac x="n" in spec)
apply (drule_tac x="xa" in spec)
apply (drule mp)
by (auto)

(* vert *)

lemma EX1_request_vert:
  "(Ev ` Alpha_pe (i, j) - Yf (i, j)) Int Ev ` Alpha_pe (Suc i, j) ~= {}
   ==> EX x. Ev (vert (Suc i, j) x) ~: Yf (i, j)"
by (auto simp add: Alpha_pe.simps)

lemma EX1_ungranted_vert_lm1:
  "[| (Ev ` Alpha_pe (i, j) - Yf (i, j)) Int Ev ` Alpha_pe (Suc i, j) ~= {} ;
       Ev ` Alpha_pe (i, j) Int Ev ` Alpha_pe (Suc i, j) <= Yf (i, j) Un Yf (Suc i, j) |]
   ==> EX x. Ev (vert (Suc i, j) x) : Yf (Suc i, j)"
by (auto simp add: Alpha_pe.simps)

lemma EX1_ungranted_vert_lm2:
  "ALL n x. (Ev (vert (Suc i, j) x) : Yf (Suc i, j) &
    (EX t. (t , Yf (Suc i, j)) : peF_rec n (Suc i, j)))
   --> (ALL x. Ev (vert (Suc i, j) x) : Yf (Suc i, j))"
apply (intro allI)
apply (induct_tac n)
apply (simp)
apply (intro allI impI)

apply (simp)
apply (simp add: Faiures_in_def)
apply (elim conjE exE disjE)
apply (force)                            (* contra *)

 (* hori *)
 apply (simp add: Faiures_in_hori_def)
 apply (elim conjE exE disjE)
 apply (force)                            (* okay *)
 apply (simp add: Faiures_out_def)
 apply (elim conjE exE disjE)
 apply (force)                            (* okay *)

  apply (simp add: Faiures_out_hori_def)
  apply (elim conjE exE disjE)
  apply (force)                            (* okay *)
  apply (force)                            (* induction *)

  apply (simp add: Faiures_out_vert_def)
  apply (elim conjE exE disjE)
  apply (force)                            (* okay *)
  apply (force)                            (* induction *)

 (* vert *)
 apply (simp add: Faiures_in_vert_def)
 apply (elim conjE exE disjE)
 apply (force)                            (* contra *)
 apply (simp add: Faiures_out_def)
 apply (elim conjE exE disjE)
 apply (force)                            (* okay *)

  apply (simp add: Faiures_out_hori_def)
  apply (elim conjE exE disjE)
  apply (force)                            (* okay *)
  apply (force)                            (* induction *)

  apply (simp add: Faiures_out_vert_def)
  apply (elim conjE exE disjE)
  apply (force)                            (* okay *)
  apply (force)                            (* induction *)
done

lemma EX1_ungranted_vert:
  "[| (Ev ` Alpha_pe (i, j) - Yf (i, j)) Int Ev ` Alpha_pe (Suc i, j) ~= {} ;
       Ev ` Alpha_pe (i, j) Int Ev ` Alpha_pe (Suc i, j) <= Yf (i, j) Un Yf (Suc i, j) ;
       (t , Yf (Suc i, j)) : peF (Suc i, j) |]
   ==> (ALL x. Ev (vert (Suc i, j) x) : Yf (Suc i, j))"
apply (insert EX1_ungranted_vert_lm1[of i j Yf])
apply (simp add: peF_def)
apply (elim conjE exE)
apply (simp)
apply (insert EX1_ungranted_vert_lm2[of i j Yf])
apply (drule_tac x="n" in spec)
apply (drule_tac x="xa" in spec)
apply (drule mp)
by (auto)

(* hori rev *)

lemma EX1_request_hori_rev:
  "(Ev ` Alpha_pe (i, Suc j) - Yf (i, Suc j)) Int Ev ` Alpha_pe (i, j) ~= {}
   ==> EX x. Ev (hori (i, Suc j) x) ~: Yf (i, Suc j)"
by (auto simp add: Alpha_pe.simps)

lemma EX1_request_hori_rev_ALL:
  "[| (Ev ` Alpha_pe (i, Suc j) - Yf (i, Suc j)) Int Ev ` Alpha_pe (i, j) ~= {} ;
      (t , Yf (i, Suc j)) : peF (i, Suc j) |]
   ==> ALL x. Ev (hori (i, Suc j) x) ~: Yf (i, Suc j)"
apply (case_tac "ALL x. Ev (hori (i, Suc j) x) ~: Yf (i, Suc j)", simp_all)
apply (simp add: peF_def)
apply (elim conjE exE)
apply (insert EX1_ungranted_hori_lm2[of i j Yf])
apply (drule_tac x="n" in spec)
apply (drule_tac x="xa" in spec)
apply (drule mp, fast)
apply (insert EX1_request_hori_rev[of i j Yf])
apply (simp)
done

lemma EX1_ungranted_hori_rev:
  "[| (Ev ` Alpha_pe (i, Suc j) - Yf (i, Suc j)) Int Ev ` Alpha_pe (i, j) ~= {} ;
       Ev ` Alpha_pe (i, Suc j) Int Ev ` Alpha_pe (i, j) <= Yf (i, Suc j) Un Yf (i, j) ;
       (t , Yf (i, Suc j)) : peF (i, Suc j) |]
   ==> ALL x. Ev (hori (i, Suc j) x) : Yf (i, j)"
apply (insert EX1_request_hori_rev_ALL[of i j Yf t])
by (auto simp add: Alpha_pe.simps)

(* vert rev *)

lemma EX1_request_vert_rev:
  "(Ev ` Alpha_pe (Suc i, j) - Yf (Suc i, j)) Int Ev ` Alpha_pe (i, j) ~= {}
   ==> EX x. Ev (vert (Suc i, j) x) ~: Yf (Suc i, j)"
by (auto simp add: Alpha_pe.simps)

lemma EX1_request_vert_rev_ALL:
  "[| (Ev ` Alpha_pe (Suc i, j) - Yf (Suc i, j)) Int Ev ` Alpha_pe (i, j) ~= {} ;
      (t , Yf (Suc i, j)) : peF (Suc i, j) |]
   ==> ALL x. Ev (vert (Suc i, j) x) ~: Yf (Suc i, j)"
apply (case_tac "ALL x. Ev (vert (Suc i, j) x) ~: Yf (Suc i, j)", simp_all)
apply (simp add: peF_def)
apply (elim conjE exE)
apply (insert EX1_ungranted_vert_lm2[of i j Yf])
apply (drule_tac x="n" in spec)
apply (drule_tac x="xa" in spec)
apply (drule mp, fast)
apply (insert EX1_request_vert_rev[of i j Yf])
apply (simp)
done

lemma EX1_ungranted_vert_rev:
  "[| (Ev ` Alpha_pe (Suc i, j) - Yf (Suc i, j)) Int Ev ` Alpha_pe (i, j) ~= {} ;
       Ev ` Alpha_pe (Suc i, j) Int Ev ` Alpha_pe (i, j) <= Yf (Suc i, j) Un Yf (i, j) ;
      (t , Yf (Suc i, j)) : peF (Suc i, j) |]
   ==> ALL x. Ev (vert (Suc i, j) x) : Yf (i, j)"
apply (insert EX1_request_vert_rev_ALL[of i j Yf t])
by (auto simp add: Alpha_pe.simps)

(*--------------------------------*
 |        making function         |
 *--------------------------------*)

(* small calculation *)

lemma EX1_cal1:
  "[| Suc (Suc (4 * x)) <= y0 ; Suc y1 <= 4 * x |]
   ==> Suc (Suc y1) < y0"
by (auto)

lemma EX1_cal1_rev:
  "[| 4 * x <= y1 ; y0 <= Suc (4 * x) |]
   ==> y0 < Suc (Suc y1)"
by (auto)

(****** hori ******)

lemma local_hori_lm:
  "[| { (peF ij, Alpha_pe ij) | ij:{(i, j), (i, Suc j)} }Fnet >>
      (i, j) --[(t, Yf),
                VocabularyOf({ (peF ij, Alpha_pe ij) | ij:Array_Index N }Fnet)]-->o
      (i, Suc j) |]
   ==> Suc (Suc (4 * lengtht (t rest-tr (range (hori (i, Suc j))))))
       <= lengtht (t rest-tr (Alpha_pe (i, j))) &
       Suc (lengtht (t rest-tr (Alpha_pe (i, Suc j))))
       <= 4 * lengtht (t rest-tr (range (hori (i, Suc j))))"
apply (simp add: isUngrantedRequestOfwrt_def)
apply (simp add: isUngrantedRequestOf_def)
apply (simp add: isRequestOf_def)
apply (simp add: isStateOf_def)
apply (elim conjE)

apply (insert local_i_j_hori[of "t rest-tr (Alpha_pe (i, j))" Yf i j])
apply (insert local_i_Suc_j_hori[of "t rest-tr (Alpha_pe (i, Suc j))" Yf i j])
apply (simp add: EX1_ungranted_hori EX1_request_hori)

apply (subgoal_tac
   "t rest-tr (Alpha_pe (i, j)) rest-tr (range (hori (i, Suc j)))
  = t rest-tr (range (hori (i, Suc j)))")
apply (subgoal_tac
  "t rest-tr (Alpha_pe (i, Suc j)) rest-tr (range (hori (i, Suc j)))
 = t rest-tr (range (hori (i, Suc j)))")
apply (simp)
apply (rule rest_tr_of_rest_tr_subset)
apply (simp add: Alpha_pe.simps image_iff, force)
apply (rule rest_tr_of_rest_tr_subset)
apply (simp add: Alpha_pe.simps image_iff, force)
done

(* local_hori *)

lemma local_hori:
  "[| { (peF ij, Alpha_pe ij) | ij:{(i, j), (i, Suc j)} }Fnet >>
      (i, j) --[(t, Yf),
                VocabularyOf({ (peF ij, Alpha_pe ij) | ij:Array_Index N }Fnet)]-->o
      (i, Suc j) |]
   ==> Suc (Suc (lengtht (t rest-tr (Alpha_pe (i, Suc j)))))
       < lengtht (t rest-tr (Alpha_pe (i, j)))"
apply (rule EX1_cal1[of "lengtht (t rest-tr (range (hori (i, Suc j))))"])
apply (simp_all add: local_hori_lm)
done

(****** vert ******)

lemma local_vert_lm:
  "[| { (peF ij, Alpha_pe ij) | ij:{(i, j), (Suc i, j)} }Fnet >>
      (i, j) --[(t, Yf),
                VocabularyOf({ (peF ij, Alpha_pe ij) | ij:Array_Index N }Fnet)]-->o
      (Suc i, j) |]
   ==> Suc (Suc (4 * lengtht (t rest-tr (range (vert (Suc i, j))))))
       <= lengtht (t rest-tr (Alpha_pe (i, j))) &
       Suc (lengtht (t rest-tr (Alpha_pe (Suc i, j))))
       <= 4 * lengtht (t rest-tr (range (vert (Suc i, j))))"
apply (simp add: isUngrantedRequestOfwrt_def)
apply (simp add: isUngrantedRequestOf_def)
apply (simp add: isRequestOf_def)
apply (simp add: isStateOf_def)
apply (elim conjE)

apply (insert local_i_j_vert[of "t rest-tr (Alpha_pe (i, j))" Yf i j])
apply (insert local_Suc_i_j_vert[of "t rest-tr (Alpha_pe (Suc i, j))" Yf i j])
apply (simp add: EX1_ungranted_vert EX1_request_vert)

apply (subgoal_tac
   "t rest-tr (Alpha_pe (i, j)) rest-tr (range (vert (Suc i, j)))
  = t rest-tr (range (vert (Suc i, j)))")
apply (subgoal_tac
  "t rest-tr (Alpha_pe (Suc i, j)) rest-tr (range (vert (Suc i, j)))
 = t rest-tr (range (vert (Suc i, j)))")
apply (simp)
apply (rule rest_tr_of_rest_tr_subset)
apply (simp add: Alpha_pe.simps image_iff, force)
apply (rule rest_tr_of_rest_tr_subset)
apply (simp add: Alpha_pe.simps image_iff, force)
done

(* local_vert *)

lemma local_vert:
  "[| { (peF ij, Alpha_pe ij) | ij:{(i, j), (Suc i, j)} }Fnet >>
      (i, j) --[(t, Yf),
                VocabularyOf({ (peF ij, Alpha_pe ij) | ij:Array_Index N }Fnet)]-->o
      (Suc i, j) |]
   ==> Suc (Suc (lengtht (t rest-tr (Alpha_pe (Suc i, j)))))
       < lengtht (t rest-tr (Alpha_pe (i, j)))"
apply (rule EX1_cal1[of "lengtht (t rest-tr (range (vert (Suc i, j))))"])
apply (simp_all add: local_vert_lm)
done

(****** hori rev ******)

lemma local_hori_rev_lm:
  "[| { (peF ij, Alpha_pe ij) | ij:{(i, Suc j), (i, j)} }Fnet >>
      (i, Suc j) --[(t, Yf),
                VocabularyOf({ (peF ij, Alpha_pe ij) | ij:Array_Index N }Fnet)]-->o
      (i, j) |]
   ==> lengtht (t rest-tr (Alpha_pe (i, j)))
       <= (Suc (4 * lengtht (t rest-tr (range (hori (i, Suc j)))))) &
       4 * lengtht (t rest-tr (range (hori (i, Suc j))))
       <= lengtht (t rest-tr (Alpha_pe (i, Suc j)))"
apply (simp add: isUngrantedRequestOfwrt_def)
apply (simp add: isUngrantedRequestOf_def)
apply (simp add: isRequestOf_def)
apply (simp add: isStateOf_def)
apply (elim conjE)

apply (insert local_i_j_hori_rev[of "t rest-tr (Alpha_pe (i, j))" Yf i j])
apply (insert local_i_Suc_j_hori_rev[of "t rest-tr (Alpha_pe (i, Suc j))" Yf i j])
apply (simp add: EX1_ungranted_hori_rev EX1_request_hori_rev)

apply (subgoal_tac
   "t rest-tr (Alpha_pe (i, j)) rest-tr (range (hori (i, Suc j)))
  = t rest-tr (range (hori (i, Suc j)))")
apply (subgoal_tac
  "t rest-tr (Alpha_pe (i, Suc j)) rest-tr (range (hori (i, Suc j)))
 = t rest-tr (range (hori (i, Suc j)))")
apply (simp)
apply (rule rest_tr_of_rest_tr_subset)
apply (simp add: Alpha_pe.simps image_iff, force)
apply (rule rest_tr_of_rest_tr_subset)
apply (simp add: Alpha_pe.simps image_iff, force)
done

(* local_hori_rev *)

lemma local_hori_rev:
  "[| { (peF ij, Alpha_pe ij) | ij:{(i, Suc j), (i, j)} }Fnet >>
      (i, Suc j) --[(t, Yf),
                VocabularyOf({ (peF ij, Alpha_pe ij) | ij:Array_Index N }Fnet)]-->o
      (i, j) |]
   ==> lengtht (t rest-tr (Alpha_pe (i, j)))
       < Suc (Suc (lengtht (t rest-tr (Alpha_pe (i, Suc j)))))"
apply (rule EX1_cal1_rev[of "lengtht (t rest-tr (range (hori (i, Suc j))))"])
apply (simp_all add: local_hori_rev_lm)
done

(****** vert rev ******)

lemma local_vert_rev_lm:
  "[| { (peF ij, Alpha_pe ij) | ij:{(Suc i, j),(i, j)} }Fnet >>
      (Suc i, j) --[(t, Yf),
                VocabularyOf({ (peF ij, Alpha_pe ij) | ij:Array_Index N }Fnet)]-->o
      (i, j) |]
   ==> lengtht (t rest-tr (Alpha_pe (i, j)))
       <= (Suc (4 * lengtht (t rest-tr (range (vert (Suc i, j)))))) &
       4 * lengtht (t rest-tr (range (vert (Suc i, j))))
       <= lengtht (t rest-tr (Alpha_pe (Suc i, j)))"
apply (simp add: isUngrantedRequestOfwrt_def)
apply (simp add: isUngrantedRequestOf_def)
apply (simp add: isRequestOf_def)
apply (simp add: isStateOf_def)
apply (elim conjE)

apply (insert local_i_j_vert_rev[of "t rest-tr (Alpha_pe (i, j))" Yf i j])
apply (insert local_Suc_i_j_vert_rev[of "t rest-tr (Alpha_pe (Suc i, j))" Yf i j])
apply (simp add: EX1_ungranted_vert_rev EX1_request_vert_rev)

apply (subgoal_tac
   "t rest-tr (Alpha_pe (i, j)) rest-tr (range (vert (Suc i, j)))
  = t rest-tr (range (vert (Suc i, j)))")
apply (subgoal_tac
  "t rest-tr (Alpha_pe (Suc i, j)) rest-tr (range (vert (Suc i, j)))
 = t rest-tr (range (vert (Suc i, j)))")
apply (simp)
apply (rule rest_tr_of_rest_tr_subset)
apply (simp add: Alpha_pe.simps image_iff, force)
apply (rule rest_tr_of_rest_tr_subset)
apply (simp add: Alpha_pe.simps image_iff, force)
done

(* local_vert_rev *)

lemma local_vert_rev:
  "[| { (peF ij, Alpha_pe ij) | ij:{(Suc i, j),(i, j)} }Fnet >>
      (Suc i, j) --[(t, Yf),
                VocabularyOf({ (peF ij, Alpha_pe ij) | ij:Array_Index N }Fnet)]-->o
      (i, j) |]
   ==> lengtht (t rest-tr (Alpha_pe (i, j)))
       < Suc (Suc (lengtht (t rest-tr (Alpha_pe (Suc i, j)))))"
apply (rule EX1_cal1_rev[of "lengtht (t rest-tr (range (vert (Suc i, j))))"])
apply (simp_all add: local_vert_rev_lm)
done

(****************** to add it again ******************)

end

author: yoshinao-isobe

repo: CSP-Prover


text:
theory DemoExamples
imports "../NonFreeInput"
begin

definition
  is_plus :: "'a :: plus \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
where
  "is_plus a b c == a + b = c"

(* we use is_plus2 to workaround that the package
   assumes that parameter conditions are only used in one instantiation *)
definition
  "is_plus2 \<equiv> is_plus"

nonfree_datatype ('a::monoid_add, 'b::monoid_add) ssum
   = Left 'a | Right 'b | Plus "('a, 'b) ssum" "('a, 'b) ssum"
where
  LeftPlus: "is_plus a1 a2 a3 ==> Plus (Left a1) (Left a2) = Left a3"
| RightPlus: "is_plus2 b1 b2 b3 ==> Plus (Right b1) (Right b2) = Right b3"
| Assoc: "Plus (Plus x1 x2) x3 = Plus x1 (Plus x2 x3)"

nonfree_primrec
  collapse_sum :: "('a :: monoid_add, 'a) ssum \<Rightarrow> 'a"
where
  "collapse_sum (Plus x1 x2) = collapse_sum x1 + collapse_sum x2"
| "collapse_sum (Left x) = x"
| "collapse_sum (Right x) = x"
apply (rule add_assoc)
by (simp add: is_plus_def is_plus2_def)+

(* trees with a finite set of subtrees *)
nonfree_datatype   'a tree = Tree "'a" "'a tfset"
        and  'a tfset = Emp | Ins "'a tree" "'a tfset"
where
  Ins1: "Ins a (Ins a s) = Ins a s"
| Ins2: "Ins a1 (Ins a2 s) = Ins a2 (Ins a1 s)"

nonfree_primrec treemap tfsetmap
where
  "treemap f (Tree a s) = Tree (f a) (tfsetmap f s)"
| "tfsetmap f Emp = Emp"
| "tfsetmap f (Ins t s) = Ins (treemap f t) (tfsetmap f s)"
by (simp add: Ins1 Ins2)+  (* discharging well-definedness *)
  (*  [| Tree |] := (% a s'. Tree (f a) s'),  [| Emp |] := Emp,  [| Ins |] := Ins *)

lemma "treemap g (treemap f t) = treemap (g o f) t"
      "tfsetmap g (tfsetmap f s) = tfsetmap (g o f) s"
apply (induct t and s)
by simp+

lemma "treemap f (Tree a (Ins t1 (Ins t2 s))) = treemap f (Tree a (Ins t2 (Ins t1 s)))"
by (simp add: Ins2)

lemma "treemap f (Tree a (Ins t (Ins t s))) = treemap f (Tree a (Ins t s))"
by (simp add: Ins1)

type_synonym var = nat

(* neq is used as a "parameter condition" on variables.
   Not defined inductively by Horn theory, but with fixed semantics. *)
definition
  neq where
  "neq x y == x ~= y"

(* lambda terms modulo alpha, with explicit substitution *)
nonfree_datatype lamterms =
    V "var" | Ap "lamterms" "lamterms" | Lm "var" "lamterms"
  | Subst "lamterms" "lamterms" "var" (* Subst X Y z = X[Y/z] *)
where
  Subst1: "Subst (V x) X x = X"
| Subst2: "neq x y ==> Subst (V x) Y y = V x"
| Subst3: "Subst (Ap X Y) Z z = Ap (Subst X Z z) (Subst Y Z z)"
| Subst4: "[| neq x y ; fresh x Y  |] ==> Subst (Lm x X) Y y = Lm x (Subst X Y y)" (* "lazily defined" *)
| fresh1: "neq x y ==> fresh x (V y)"
| fresh2: "[| fresh x Y ; fresh x Z |] ==> fresh x (Ap Y Z)"
| fresh3: "fresh x (Lm x X)"
| fresh4: "fresh x Y ==> fresh x (Lm y Y)"
| alpha:  "[| neq y x ; fresh y X |] ==> Lm x X = Lm y (Subst X (V y) x)"

(* Count number of occurrences of a variable in a lamterm.
   More precisely: construct occurence counter for given lamterm.
   Note: variable to be counted changes in rec. calls!
   Not a parameter of iter definition. *)
nonfree_primrec
  numoccs :: "lamterms => (var => nat)"
where
  "numoccs (V x) = (% z.      if x = z then 1 else 0)"
| "numoccs (Ap X Y)  = (% z.  numoccs X z + numoccs Y z)"
| "numoccs (Lm x X) = (% z.   if x = z then 0 else numoccs X z)"
| "numoccs (Subst X Y y) = (% z.
     if y = z then numoccs X y * numoccs Y z
     else numoccs X z + numoccs X y * numoccs Y z)"
| "fresh x X ==> numoccs X x = 0"
  apply (rule ext, simp add: neq_def Nat.add_mult_distrib)+
  apply auto
  apply (rule ext, simp add: neq_def)+
  by (auto simp add: neq_def Nat.add_mult_distrib)

lemma "neq y x ==> fresh y X ==> numoccs (Lm x X) z = numoccs (Lm y (Subst X (V y) x)) z"
  by (simp add: alpha)

lemma "fresh x X ==> numoccs X x = 0"
  by simp

end

author: metaforcy

repo: nonfree-data


text:
\<^marker>\<open>creator Bilel Ghorbel, Florian Kessler\<close>
section "Big step semantics of IMP-"
theory Big_StepT imports Main Com begin

paragraph "Summary"
text\<open>We define big step semantics with time for IMP-.
Based on the big step semantics definition with time of IMP\<close>

subsection "Big step semantics definition:"

text "In IMP- Branching is only based on whether a variable's value equals 0."

inductive
  big_step_t :: "com \<times> state \<Rightarrow> nat \<Rightarrow> state \<Rightarrow> bool"  ("_ \<Rightarrow>\<^bsup> _ \<^esup> _" 55)
where
Skip: "(SKIP,s) \<Rightarrow>\<^bsup> Suc (0::nat) \<^esup> s"|
Assign: "(x ::= a,s) \<Rightarrow>\<^bsup> Suc (Suc 0) \<^esup> s(x := aval a s)" |
Seq: "\<lbrakk> (c1,s1) \<Rightarrow>\<^bsup> x \<^esup> s2;  (c2,s2) \<Rightarrow>\<^bsup> y \<^esup> s3 ; z=x+y \<rbrakk> \<Longrightarrow> (c1;;c2, s1) \<Rightarrow>\<^bsup> z \<^esup> s3" |
IfTrue: "\<lbrakk> s b \<noteq> 0;  (c1,s) \<Rightarrow>\<^bsup> x \<^esup> t; y=x+1 \<rbrakk> \<Longrightarrow> (IF b \<noteq>0 THEN c1 ELSE c2, s) \<Rightarrow>\<^bsup> y \<^esup> t" |
IfFalse: "\<lbrakk> s b = 0; (c2,s) \<Rightarrow>\<^bsup> x \<^esup> t; y=x+1  \<rbrakk> \<Longrightarrow> (IF b \<noteq>0 THEN c1 ELSE c2, s) \<Rightarrow>\<^bsup> y \<^esup> t" |
WhileFalse: "\<lbrakk> s b = 0 \<rbrakk> \<Longrightarrow> (WHILE b \<noteq>0 DO c,s) \<Rightarrow>\<^bsup> Suc (Suc 0) \<^esup> s" |
WhileTrue: "\<lbrakk> s1 b \<noteq> 0;  (c,s1) \<Rightarrow>\<^bsup> x \<^esup> s2;  (WHILE b \<noteq>0 DO c, s2) \<Rightarrow>\<^bsup> y \<^esup> s3; 1+x+y=z  \<rbrakk>
    \<Longrightarrow> (WHILE b \<noteq>0 DO c, s1) \<Rightarrow>\<^bsup> z \<^esup> s3"

bundle big_step_syntax
begin
notation big_step_t ("_ \<Rightarrow>\<^bsup> _ \<^esup> _" 55)
end

bundle no_big_step_syntax
begin
no_notation big_step_t ("_ \<Rightarrow>\<^bsup> _ \<^esup> _" 55)
end

code_pred big_step_t .

text "Some examples using the big step semantics"
experiment
begin

text "finding out the final state and running time of a command:"
schematic_goal ex: "(''x'' ::= A (N 5);; ''y'' ::= A (V ''x''), s) \<Rightarrow>\<^bsup> ?t \<^esup> ?s"
  apply(rule Seq)
    apply(rule Assign)
   apply simp
   apply(rule Assign)
  apply simp
  done

values "{(t, x). big_step_t (SKIP, \<lambda>_. 0) x t}"

values "{map t [''x''] |t x. (SKIP, <''x'' := 42>) \<Rightarrow>\<^bsup> x \<^esup> t}"

values "{map t [''x''] |t x. (''x'' ::=A (N 2), <''x'' := 42>) \<Rightarrow>\<^bsup> x \<^esup> t}"

values "{(map t [''x''],x) |t x. (WHILE ''x''\<noteq>0 DO ''x''::= Sub (V ''x'') (N 1),<''x'':=5>) \<Rightarrow>\<^bsup> x \<^esup> t }"

end

text "proof automation:"

text "Introduction rules:"
declare big_step_t.intros [intro]

text "Induction rules with pair splitting"
lemmas big_step_t_induct = big_step_t.induct[split_format(complete)]

subsection "Rule inversion"
inductive_cases Skip_tE[elim!]: "(SKIP,s) \<Rightarrow>\<^bsup> x \<^esup> t"
inductive_cases Assign_tE[elim!]: "(x ::= a,s) \<Rightarrow>\<^bsup> p \<^esup> t"
inductive_cases Seq_tE[elim!]: "(c1;;c2,s1) \<Rightarrow>\<^bsup> p \<^esup> s3"
inductive_cases If_tE[elim!]: "(IF b \<noteq>0 THEN c1 ELSE c2,s) \<Rightarrow>\<^bsup> x \<^esup> t"
inductive_cases While_tE[elim]: "(WHILE b \<noteq>0 DO c,s) \<Rightarrow>\<^bsup> x \<^esup> t"

text "Rule inversion use examples:"
lemma "(IF b \<noteq>0 THEN SKIP ELSE SKIP, s) \<Rightarrow>\<^bsup> x \<^esup> t \<Longrightarrow> t = s"
  by blast

lemma assumes "(IF b \<noteq>0 THEN SKIP ELSE SKIP, s) \<Rightarrow>\<^bsup> x \<^esup> t"
  shows "t = s"
  using assms apply cases by auto

subsection "Determinism of Big semantics of IMP-"
theorem big_step_t_determ2: "\<lbrakk> (c,s) \<Rightarrow>\<^bsup> p \<^esup> t; (c,s) \<Rightarrow>\<^bsup> q \<^esup> u \<rbrakk> \<Longrightarrow> (u = t \<and> p=q)"
  apply  (induction arbitrary: u q rule: big_step_t_induct)
    apply(elim Skip_tE) apply(simp)
    apply(elim Assign_tE) apply(simp)
  apply blast
    apply(elim If_tE) apply(simp) apply blast
    apply(elim If_tE)  apply (linarith) apply simp
    apply(erule While_tE) apply(simp) apply simp
  subgoal premises p for s1 b c x s2 y s3 z u q
    using p(7) apply(safe)
      apply(erule While_tE)
        using p(1-6) apply fast
        using p(1-6) apply (simp)
      apply(erule While_tE)
        using p(1-6) apply fast
        using p(1-6) by (simp)
done

lemma bigstep_det: "(c1, s) \<Rightarrow>\<^bsup> p1 \<^esup> t1 \<Longrightarrow> (c1, s) \<Rightarrow>\<^bsup> p \<^esup> t \<Longrightarrow> p1=p \<and> t1=t"
  using big_step_t_determ2 by simp

subsection "Progress property"
text "every command costs time"
lemma bigstep_progress: "(c, s) \<Rightarrow>\<^bsup> p \<^esup> t \<Longrightarrow> p > 0"
  apply(induct rule: big_step_t.induct, auto) done

subsection "abbreviations and properties"
abbreviation terminates ("\<down>") where "terminates cs \<equiv> (\<exists>n a. (cs \<Rightarrow>\<^bsup> n \<^esup> a))"
abbreviation thestate ("\<down>\<^sub>s") where "thestate cs \<equiv> (THE a. \<exists>n. (cs \<Rightarrow>\<^bsup> n \<^esup> a))"
abbreviation thetime ("\<down>\<^sub>t") where "thetime cs \<equiv> (THE n. \<exists>a. (cs \<Rightarrow>\<^bsup> n \<^esup> a))"

lemma bigstepT_the_cost: "(c, s) \<Rightarrow>\<^bsup> t \<^esup> s' \<Longrightarrow> \<down>\<^sub>t(c, s) = t"
  using bigstep_det by blast

lemma bigstepT_the_state: "(c, s) \<Rightarrow>\<^bsup> t \<^esup> s' \<Longrightarrow> \<down>\<^sub>s(c, s) = s'"
  using bigstep_det by blast

lemma SKIPnot: "(\<not> (SKIP, s) \<Rightarrow>\<^bsup> p \<^esup> t) \<longleftrightarrow> (s\<noteq>t \<or> p\<noteq>Suc 0)" by blast

lemma SKIPp: "\<down>\<^sub>t(SKIP,s) = Suc 0"
  apply(rule the_equality)
  apply fast
  apply auto done

lemma SKIPt: "\<down>\<^sub>s(SKIP,s) = s"
  apply(rule the_equality)
  apply fast
  apply auto done

lemma ASSp: "(THE p. Ex (big_step_t (x ::= e, s) p)) = Suc(Suc 0)"
  apply(rule the_equality)
  apply fast
  apply auto done

lemma ASSt: "(THE t. \<exists>p. (x ::= e, s) \<Rightarrow>\<^bsup> p \<^esup> t) = s(x := aval e s)"
  apply(rule the_equality)
  apply fast
  apply auto done

lemma ASSnot: "( \<not> (x ::= e, s) \<Rightarrow>\<^bsup> p \<^esup> t ) = (p\<noteq>Suc(Suc 0) \<or> t\<noteq>s(x := aval e s))"
  apply auto done

lemma If_THE_True: "Suc (THE n. \<exists>a. (c1, s) \<Rightarrow>\<^bsup> n \<^esup> a) =  (THE n. \<exists>a. (IF b \<noteq>0 THEN c1 ELSE c2, s) \<Rightarrow>\<^bsup> n \<^esup> a)"
     if T: "s b \<noteq> 0" and c1_t: "terminates (c1,s)" for s l
proof -
  from c1_t obtain p t where a: "(c1, s) \<Rightarrow>\<^bsup> p \<^esup> t" by blast
  with T have b: "(IF b \<noteq>0 THEN c1 ELSE c2, s) \<Rightarrow>\<^bsup> p+1 \<^esup> t"  using IfTrue by simp
  from a bigstepT_the_cost have "(THE n. \<exists>a. (c1, s) \<Rightarrow>\<^bsup> n \<^esup> a) = p" by simp
  moreover from b bigstepT_the_cost have "(THE n. \<exists>a. (IF b \<noteq>0 THEN c1 ELSE c2, s) \<Rightarrow>\<^bsup> n \<^esup> a) = p+1" by simp
  ultimately show ?thesis by simp
qed

lemma If_THE_False:
 "Suc (THE n. \<exists>a. (c2, s) \<Rightarrow>\<^bsup> n \<^esup> a) =  (THE n. \<exists>a. (IF b \<noteq>0 THEN c1 ELSE c2, s) \<Rightarrow>\<^bsup> n \<^esup> a)"
     if T: "s b = 0" and c2_t: "\<down> (c2,s)" for s l
proof -
  from c2_t obtain p t where a: "(c2, s) \<Rightarrow>\<^bsup> p \<^esup> t"  by blast
  with T have b: "(IF b \<noteq>0 THEN c1 ELSE c2, s) \<Rightarrow>\<^bsup> p+1 \<^esup> t"  using IfFalse by simp
  from a bigstepT_the_cost have "(THE n. \<exists>a. (c2, s) \<Rightarrow>\<^bsup> n \<^esup> a) = p" by simp
  moreover from b bigstepT_the_cost have "(THE n. \<exists>a. (IF b \<noteq>0 THEN c1 ELSE c2, s) \<Rightarrow>\<^bsup> n \<^esup> a) = p+1" by simp
  ultimately show ?thesis by simp
qed

end

author: wimmers

repo: poly-reductions


text:
\<^marker>\<open>creator "Kevin Kappelmann"\<close>
subsection \<open>Basic Setup\<close>
theory Transport_Base
  imports
    HOL_Basics.Galois_Equivalences
    HOL_Basics.Galois_Relator
begin

paragraph \<open>Summary\<close>
text \<open>Basic setup for commonly used concepts in Transport, including a suitable
locale.\<close>

locale transport = galois L R l r
  for L :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
  and R :: "'b \<Rightarrow> 'b \<Rightarrow> bool"
  and l :: "'a \<Rightarrow> 'b"
  and r :: "'b \<Rightarrow> 'a"
begin

subsubsection \<open>Ordered Galois Connections\<close>

definition "preorder_galois_connection \<equiv>
  ((\<le>\<^bsub>L\<^esub>) \<stileturn> (\<le>\<^bsub>R\<^esub>)) l r
  \<and> preorder_on (in_field (\<le>\<^bsub>L\<^esub>)) (\<le>\<^bsub>L\<^esub>)
  \<and> preorder_on (in_field (\<le>\<^bsub>R\<^esub>)) (\<le>\<^bsub>R\<^esub>)"

notation transport.preorder_galois_connection (infix "\<stileturn>\<^bsub>pre\<^esub>" 50)

lemma preorder_galois_connectionI [intro]:
  assumes "((\<le>\<^bsub>L\<^esub>) \<stileturn> (\<le>\<^bsub>R\<^esub>)) l r"
  and "preorder_on (in_field (\<le>\<^bsub>L\<^esub>)) (\<le>\<^bsub>L\<^esub>)"
  and "preorder_on (in_field (\<le>\<^bsub>R\<^esub>)) (\<le>\<^bsub>R\<^esub>)"
  shows "((\<le>\<^bsub>L\<^esub>) \<stileturn>\<^bsub>pre\<^esub> (\<le>\<^bsub>R\<^esub>)) l r"
  unfolding preorder_galois_connection_def using assms by blast

lemma preorder_galois_connectionE [elim]:
  assumes "((\<le>\<^bsub>L\<^esub>) \<stileturn>\<^bsub>pre\<^esub> (\<le>\<^bsub>R\<^esub>)) l r"
  obtains "((\<le>\<^bsub>L\<^esub>) \<stileturn> (\<le>\<^bsub>R\<^esub>)) l r" "preorder_on (in_field (\<le>\<^bsub>L\<^esub>)) (\<le>\<^bsub>L\<^esub>)"
    "preorder_on (in_field (\<le>\<^bsub>R\<^esub>)) (\<le>\<^bsub>R\<^esub>)"
  using assms unfolding preorder_galois_connection_def by blast

context
begin

interpretation t : transport S T f g for S T f g .

lemma rel_inv_preorder_galois_connection_eq_preorder_galois_connection_rel_inv [simp]:
  "((\<le>\<^bsub>R\<^esub>) \<stileturn>\<^bsub>pre\<^esub> (\<le>\<^bsub>L\<^esub>))\<inverse> = ((\<ge>\<^bsub>L\<^esub>) \<stileturn>\<^bsub>pre\<^esub> (\<ge>\<^bsub>R\<^esub>))"
  by (intro ext) (auto intro!: t.preorder_galois_connectionI)

end

corollary preorder_galois_connection_rel_inv_iff_preorder_galois_connection [iff]:
  "((\<ge>\<^bsub>L\<^esub>) \<stileturn>\<^bsub>pre\<^esub> (\<ge>\<^bsub>R\<^esub>)) l r \<longleftrightarrow> ((\<le>\<^bsub>R\<^esub>) \<stileturn>\<^bsub>pre\<^esub> (\<le>\<^bsub>L\<^esub>)) r l"
  by (simp flip:
    rel_inv_preorder_galois_connection_eq_preorder_galois_connection_rel_inv)

definition "partial_equivalence_rel_galois_connection \<equiv>
  ((\<le>\<^bsub>L\<^esub>) \<stileturn> (\<le>\<^bsub>R\<^esub>)) l r
  \<and> partial_equivalence_rel (\<le>\<^bsub>L\<^esub>)
  \<and> partial_equivalence_rel (\<le>\<^bsub>R\<^esub>)"

notation transport.partial_equivalence_rel_galois_connection (infix "\<stileturn>\<^bsub>PER\<^esub>" 50)

lemma partial_equivalence_rel_galois_connectionI [intro]:
  assumes "((\<le>\<^bsub>L\<^esub>) \<stileturn> (\<le>\<^bsub>R\<^esub>)) l r"
  and "partial_equivalence_rel_on (in_field (\<le>\<^bsub>L\<^esub>)) (\<le>\<^bsub>L\<^esub>)"
  and "partial_equivalence_rel_on (in_field (\<le>\<^bsub>R\<^esub>)) (\<le>\<^bsub>R\<^esub>)"
  shows "((\<le>\<^bsub>L\<^esub>) \<stileturn>\<^bsub>PER\<^esub> (\<le>\<^bsub>R\<^esub>)) l r"
  unfolding partial_equivalence_rel_galois_connection_def using assms by blast

lemma partial_equivalence_rel_galois_connectionE [elim]:
  assumes "((\<le>\<^bsub>L\<^esub>) \<stileturn>\<^bsub>PER\<^esub> (\<le>\<^bsub>R\<^esub>)) l r"
  obtains "((\<le>\<^bsub>L\<^esub>) \<stileturn>\<^bsub>pre\<^esub> (\<le>\<^bsub>R\<^esub>)) l r" "symmetric (\<le>\<^bsub>L\<^esub>)" "symmetric (\<le>\<^bsub>R\<^esub>)"
  using assms unfolding partial_equivalence_rel_galois_connection_def by blast

context
begin

interpretation t : transport S T f g for S T f g .

lemma rel_inv_partial_equivalence_rel_galois_connection_eq_partial_equivalence_rel_galois_connection_rel_inv
  [simp]: "((\<le>\<^bsub>R\<^esub>) \<stileturn>\<^bsub>PER\<^esub> (\<le>\<^bsub>L\<^esub>))\<inverse> = ((\<ge>\<^bsub>L\<^esub>) \<stileturn>\<^bsub>PER\<^esub> (\<ge>\<^bsub>R\<^esub>))"
  by (intro ext) blast

end

corollary partial_equivalence_rel_galois_connection_rel_inv_iff_partial_equivalence_rel_galois_connection
  [iff]: "((\<ge>\<^bsub>L\<^esub>) \<stileturn>\<^bsub>PER\<^esub> (\<ge>\<^bsub>R\<^esub>)) l r \<longleftrightarrow> ((\<le>\<^bsub>R\<^esub>) \<stileturn>\<^bsub>PER\<^esub> (\<le>\<^bsub>L\<^esub>)) r l"
  by (simp flip:
    rel_inv_partial_equivalence_rel_galois_connection_eq_partial_equivalence_rel_galois_connection_rel_inv)

lemma Galois_comp_rel_inv_Galois_eq_left_if_partial_equivalence_rel_galois_connection:
  assumes "((\<le>\<^bsub>L\<^esub>) \<stileturn>\<^bsub>PER\<^esub> (\<le>\<^bsub>R\<^esub>)) l r"
  shows "((\<^bsub>L\<^esub>\<lessapprox>) \<circ>\<circ> (\<greaterapprox>\<^bsub>L\<^esub>)) = (\<le>\<^bsub>L\<^esub>)"
proof (intro ext iffI)
  fix x x' assume "((\<^bsub>L\<^esub>\<lessapprox>) \<circ>\<circ> (\<greaterapprox>\<^bsub>L\<^esub>)) x x'"
  then obtain y where "x \<le>\<^bsub>L\<^esub> r y" "r y \<ge>\<^bsub>L\<^esub> x'" by blast
  moreover with assms have "r y \<le>\<^bsub>L\<^esub> x'" by (blast dest: symmetricD)
  ultimately show "x \<le>\<^bsub>L\<^esub> x'" using assms by blast
next
  fix x x' assume "x \<le>\<^bsub>L\<^esub> x'"
  with assms have "x \<^bsub>L\<^esub>\<lessapprox> l x'" "x' \<^bsub>L\<^esub>\<lessapprox> l x'"
    by (blast intro: Galois_left_if_left_relI)+
  moreover with assms have "l x' \<lessapprox>\<^bsub>L\<^esub> x'"
    by (subst Galois_rel_inv_eq_Galois_if_in_codom_eq_in_dom_if_symmetric)
    (blast intro: in_codom_eq_in_dom_if_partial_equivalence_rel)+
  ultimately show "((\<^bsub>L\<^esub>\<lessapprox>) \<circ>\<circ> (\<greaterapprox>\<^bsub>L\<^esub>)) x x'" by blast
qed

subsubsection \<open>Ordered Equivalences\<close>

definition "preorder_equivalence \<equiv>
  ((\<le>\<^bsub>L\<^esub>) \<equiv>\<^sub>G (\<le>\<^bsub>R\<^esub>)) l r
  \<and> preorder_on (in_field (\<le>\<^bsub>L\<^esub>)) (\<le>\<^bsub>L\<^esub>)
  \<and> preorder_on (in_field (\<le>\<^bsub>R\<^esub>)) (\<le>\<^bsub>R\<^esub>)"

notation transport.preorder_equivalence (infix "\<equiv>\<^bsub>pre\<^esub>" 50)

lemma preorder_equivalence_if_galois_equivalenceI [intro]:
  assumes "((\<le>\<^bsub>L\<^esub>) \<equiv>\<^sub>G (\<le>\<^bsub>R\<^esub>)) l r"
  and "preorder_on (in_field (\<le>\<^bsub>L\<^esub>)) (\<le>\<^bsub>L\<^esub>)"
  and "preorder_on (in_field (\<le>\<^bsub>R\<^esub>)) (\<le>\<^bsub>R\<^esub>)"
  shows "((\<le>\<^bsub>L\<^esub>) \<equiv>\<^bsub>pre\<^esub> (\<le>\<^bsub>R\<^esub>)) l r"
  unfolding preorder_equivalence_def using assms by blast

lemma preorder_equivalence_if_order_equivalenceI:
  assumes "((\<le>\<^bsub>L\<^esub>) \<equiv>\<^sub>o (\<le>\<^bsub>R\<^esub>)) l r"
  and "transitive (\<le>\<^bsub>L\<^esub>)"
  and "transitive (\<le>\<^bsub>R\<^esub>)"
  shows "((\<le>\<^bsub>L\<^esub>) \<equiv>\<^bsub>pre\<^esub> (\<le>\<^bsub>R\<^esub>)) l r"
  unfolding preorder_equivalence_def using assms
  by (blast intro: reflexive_on_in_field_if_transitive_if_rel_equivalence_on
    dest: galois_equivalence_left_right_if_transitive_if_order_equivalence)

lemma preorder_equivalence_galois_equivalenceE [elim]:
  assumes "((\<le>\<^bsub>L\<^esub>) \<equiv>\<^bsub>pre\<^esub> (\<le>\<^bsub>R\<^esub>)) l r"
  obtains "((\<le>\<^bsub>L\<^esub>) \<equiv>\<^sub>G (\<le>\<^bsub>R\<^esub>)) l r" "preorder_on (in_field (\<le>\<^bsub>L\<^esub>)) (\<le>\<^bsub>L\<^esub>)"
    "preorder_on (in_field (\<le>\<^bsub>R\<^esub>)) (\<le>\<^bsub>R\<^esub>)"
  using assms unfolding preorder_equivalence_def by blast

lemma preorder_equivalence_order_equivalenceE:
  assumes "((\<le>\<^bsub>L\<^esub>) \<equiv>\<^bsub>pre\<^esub> (\<le>\<^bsub>R\<^esub>)) l r"
  obtains "((\<le>\<^bsub>L\<^esub>) \<equiv>\<^sub>o (\<le>\<^bsub>R\<^esub>)) l r" "preorder_on (in_field (\<le>\<^bsub>L\<^esub>)) (\<le>\<^bsub>L\<^esub>)"
    "preorder_on (in_field (\<le>\<^bsub>R\<^esub>)) (\<le>\<^bsub>R\<^esub>)"
  using assms by (blast intro:
    order_equivalence_if_reflexive_on_in_field_if_galois_equivalence)

context
begin

interpretation t : transport S T f g for S T f g .

lemma rel_inv_preorder_equivalence_eq_preorder_equivalence [simp]:
  "((\<le>\<^bsub>R\<^esub>) \<equiv>\<^bsub>pre\<^esub> (\<le>\<^bsub>L\<^esub>))\<inverse> = ((\<le>\<^bsub>L\<^esub>) \<equiv>\<^bsub>pre\<^esub> (\<le>\<^bsub>R\<^esub>))"
  by (intro ext) blast

end

corollary preorder_equivalence_right_left_iff_preorder_equivalence_left_right:
  "((\<le>\<^bsub>R\<^esub>) \<equiv>\<^bsub>pre\<^esub> (\<le>\<^bsub>L\<^esub>)) r l \<longleftrightarrow> ((\<le>\<^bsub>L\<^esub>) \<equiv>\<^bsub>pre\<^esub> (\<le>\<^bsub>R\<^esub>)) l r"
  by (simp flip: rel_inv_preorder_equivalence_eq_preorder_equivalence)

lemma preorder_equivalence_rel_inv_eq_preorder_equivalence [simp]:
  "((\<ge>\<^bsub>L\<^esub>) \<equiv>\<^bsub>pre\<^esub> (\<ge>\<^bsub>R\<^esub>)) = ((\<le>\<^bsub>L\<^esub>) \<equiv>\<^bsub>pre\<^esub> (\<le>\<^bsub>R\<^esub>))"
  by (intro ext iffI)
  (auto intro!: transport.preorder_equivalence_if_galois_equivalenceI
    elim!: transport.preorder_equivalence_galois_equivalenceE)

definition "partial_equivalence_rel_equivalence \<equiv>
  ((\<le>\<^bsub>L\<^esub>) \<equiv>\<^sub>G (\<le>\<^bsub>R\<^esub>)) l r
  \<and> partial_equivalence_rel (\<le>\<^bsub>L\<^esub>)
  \<and> partial_equivalence_rel (\<le>\<^bsub>R\<^esub>)"

notation transport.partial_equivalence_rel_equivalence (infix "\<equiv>\<^bsub>PER\<^esub>" 50)

lemma partial_equivalence_rel_equivalence_if_galois_equivalenceI [intro]:
  assumes "((\<le>\<^bsub>L\<^esub>) \<equiv>\<^sub>G (\<le>\<^bsub>R\<^esub>)) l r"
  and "partial_equivalence_rel (\<le>\<^bsub>L\<^esub>)"
  and "partial_equivalence_rel (\<le>\<^bsub>R\<^esub>)"
  shows "((\<le>\<^bsub>L\<^esub>) \<equiv>\<^bsub>PER\<^esub> (\<le>\<^bsub>R\<^esub>)) l r"
  unfolding partial_equivalence_rel_equivalence_def using assms by blast

lemma partial_equivalence_rel_equivalence_if_order_equivalenceI:
  assumes "((\<le>\<^bsub>L\<^esub>) \<equiv>\<^sub>o (\<le>\<^bsub>R\<^esub>)) l r"
  and "partial_equivalence_rel (\<le>\<^bsub>L\<^esub>)"
  and "partial_equivalence_rel (\<le>\<^bsub>R\<^esub>)"
  shows "((\<le>\<^bsub>L\<^esub>) \<equiv>\<^bsub>PER\<^esub> (\<le>\<^bsub>R\<^esub>)) l r"
  unfolding partial_equivalence_rel_equivalence_def using assms
  by (blast dest: galois_equivalence_left_right_if_transitive_if_order_equivalence)

lemma partial_equivalence_rel_equivalenceE [elim]:
  assumes "((\<le>\<^bsub>L\<^esub>) \<equiv>\<^bsub>PER\<^esub> (\<le>\<^bsub>R\<^esub>)) l r"
  obtains "((\<le>\<^bsub>L\<^esub>) \<equiv>\<^bsub>pre\<^esub> (\<le>\<^bsub>R\<^esub>)) l r" "symmetric (\<le>\<^bsub>L\<^esub>)" "symmetric (\<le>\<^bsub>R\<^esub>)"
  using assms unfolding partial_equivalence_rel_equivalence_def by blast

context
begin

interpretation t : transport S T f g for S T f g .

lemma rel_inv_partial_equivalence_rel_equivalence_eq_partial_equivalence_rel_equivalence [simp]:
  "((\<le>\<^bsub>R\<^esub>) \<equiv>\<^bsub>PER\<^esub> (\<le>\<^bsub>L\<^esub>))\<inverse> = ((\<le>\<^bsub>L\<^esub>) \<equiv>\<^bsub>PER\<^esub> (\<le>\<^bsub>R\<^esub>))"
  by (intro ext) blast

end

corollary partial_equivalence_rel_equivalence_right_left_iff_partial_equivalence_rel_equivalence_left_right:
  "((\<le>\<^bsub>R\<^esub>) \<equiv>\<^bsub>PER\<^esub> (\<le>\<^bsub>L\<^esub>)) r l \<longleftrightarrow> ((\<le>\<^bsub>L\<^esub>) \<equiv>\<^bsub>PER\<^esub> (\<le>\<^bsub>R\<^esub>)) l r"
  by (simp flip:
    rel_inv_partial_equivalence_rel_equivalence_eq_partial_equivalence_rel_equivalence)

lemma partial_equivalence_rel_equivalence_rel_inv_eq_partial_equivalence_rel_equivalence
  [simp]: "((\<ge>\<^bsub>L\<^esub>) \<equiv>\<^bsub>PER\<^esub> (\<ge>\<^bsub>R\<^esub>)) = ((\<le>\<^bsub>L\<^esub>) \<equiv>\<^bsub>PER\<^esub> (\<le>\<^bsub>R\<^esub>))"
  by (intro ext iffI)
  (auto intro!: transport.partial_equivalence_rel_equivalence_if_galois_equivalenceI
    elim!: transport.partial_equivalence_rel_equivalenceE
      transport.preorder_equivalence_galois_equivalenceE
      preorder_on_in_fieldE)

end

end

author: kappelmann

repo: transport-isabelle


text:
(*
 * Copyright 2016, NICTA
 *
 * This software may be distributed and modified according to the terms of
 * the GNU General Public License version 2. Note that NO WARRANTY is provided.
 * See "LICENSE_GPLv2.txt" for details.
 *
 * @TAG(NICTA_GPL)
 *)

theory WordArrayT
imports
  "../adt/BilbyT"
  "../lib/Loops"
begin

consts \<alpha>wa :: "'a WordArray \<Rightarrow> 'a list"
consts make :: "'a list \<Rightarrow> 'a WordArray"

definition
  mapAccumObs :: "nat \<Rightarrow> nat \<Rightarrow> (('a, 'acc, 'obsv) ElemAO \<Rightarrow> ('a \<times> 'acc))
   \<Rightarrow> 'a list \<Rightarrow> 'acc \<Rightarrow> 'obsv \<Rightarrow> 'a list \<times> 'acc"
where
  "mapAccumObs frm to fn xs vacc obs =
   (let (ys, acc) = fold (\<lambda>elem (ys,acc).
           let (elem,acc) = fn (ElemAO.make elem acc obs)
            in  (ys@[elem], acc)) (slice frm to xs) ([],vacc)
     in (take frm xs @ ys @ drop (max frm to) xs, acc))"

lemma length_mapAccum_helper:
  "length (fst $ fold (\<lambda>x (ys,a'). let  (elem, acc) = loopbody x a'
                                  in  (ys@[elem],acc)) (xs) (ys,a)
           )
         = length ys + length xs"
  by (induct xs arbitrary: a ys, auto simp: Let_def slice_def  split: prod.split)

lemma length_mapAccum_slice_helper:
  "length (let (xs', _) = fold (\<lambda>x (ys,a'). let  (elem, acc) = loopbody x a'
                                  in  (ys@[elem],acc)) (slice frm to xs) (ys,a)
           in xs') = length ys + length (slice frm to xs)"
proof -
  have f1: "(\<lambda>x (ys, a'). (ys @ [TypBucket.fst (loopbody x a')], TypBucket.snd (loopbody x a'))) =
            (\<lambda>x prod. (TypBucket.fst prod @ [TypBucket.fst (loopbody x (TypBucket.snd prod))], TypBucket.snd (loopbody x (TypBucket.snd prod))))"
    using split_beta by blast
  show ?thesis
    apply simp
    apply (simp only: Let_def prod.case_eq_if)
    using length_mapAccum_helper[unfolded fun_app_def prod.case_eq_if Let_def]
    apply (force simp add: f1)
    done
qed

lemma slice_length:
 "length (slice frm to xs) = min (to - frm) (length xs - frm)"
 by (simp add: slice_def)

lemma length_mapAccum_slice_helper':
  "length (take frm xs @ fst (let (xs', acc) = fold (\<lambda>x (ys,a'). let  (elem, acc) = loopbody x a'
                                  in  (ys@[elem],acc)) (slice frm to xs) (ys,a)
           in (xs',acc))  @ List.drop (max frm to) xs) = length ys + length xs"
  unfolding Let_def  prod.case_eq_if
  using length_mapAccum_slice_helper[unfolded prod.case_eq_if Let_def, where xs=xs and ys=ys and frm=frm and to=to and loopbody=loopbody and a=a]
  by (simp add: slice_length)

lemma length_mapAccum:
  "length (fst (mapAccumObs frm to fn xs a obs)) = length xs"
  unfolding mapAccumObs_def
  using length_mapAccum_slice_helper'[where frm=frm and to=to and xs=xs and a=a and ys="[]"]
  by (auto simp: Let_def prod.case_eq_if)

lemma length_mapAccumI:
  " P (length xs) \<Longrightarrow> P (length (fst (mapAccumObs frm to fn xs a obs)))"
 by (simp add : length_mapAccum)

axiomatization
where
  wordarray_make: "\<And>xs. \<alpha>wa (WordArrayT.make xs) = xs"
 and
  wordarray_make': "\<And>wa. WordArrayT.make (\<alpha>wa wa) = wa"
 and
  wordarray_create_ret:
   "\<And>P.\<lbrakk>  \<And>ex'. (ex', Option.None ()) = malloc ex \<Longrightarrow> P (Error ex');
           \<And>ex' v. \<lbrakk> sz > 0 ; (ex', Option.Some v) = malloc ex; length (\<alpha>wa v) = unat sz \<rbrakk> \<Longrightarrow>
                 P (Success (ex', v))
        \<rbrakk> \<Longrightarrow>
      P (wordarray_create (ex, sz))"

   and wordarray_length_ret:
   "unat (wordarray_length arr) = length (\<alpha>wa arr)"

  and wordarray_get_ret:
  "\<lbrakk> unat index < length (\<alpha>wa arr) \<rbrakk> \<Longrightarrow>
    wordarray_get (arr, index) = \<alpha>wa arr ! unat index"

  and wordarray_modify_ret:
   "\<And>P. \<lbrakk> unat index < List.length (\<alpha>wa varr);
       let r = modifier (ElemAO.make ((\<alpha>wa varr)!unat index) vacc obs) in
       P (ArrA.make (WordArrayT.make ((\<alpha>wa varr)[unat index:=ElemA.elem\<^sub>f r])) (ElemA.acc\<^sub>f r)) \<rbrakk> \<Longrightarrow>
        P (wordarray_modify (\<lparr>ArrayUseValueP.arr\<^sub>f = varr, idx\<^sub>f =  index, f\<^sub>f = modifier, acc\<^sub>f = vacc, obsv\<^sub>f = obs \<rparr>))"
(* Alternative that does not use WordArray.make
  and wordarray_modify_ret:
   "\<And>P. \<lbrakk> unat index < List.length (\<alpha>wa varr);
       ElemA.make a acc'' = modifier (ElemAO.make ((\<alpha>wa varr)!unat index) vacc obs);
       \<And>arr'. \<alpha>wa arr' = (\<alpha>wa varr)[unat index:=a] \<Longrightarrow> P (ArrA.make arr' acc'') \<rbrakk> \<Longrightarrow>
        P (wordarray_modify (ArrayUseValueP.make varr index modifier vacc obs))"
*)
   and wordarray_map_no_break_ret:
   "\<And>P. (let (aarr, vacc) = mapAccumObs (unat frm) (unat to) body (\<alpha>wa arr) acc obs
          in P ((WordArrayT.make aarr), vacc))
   \<Longrightarrow> P (wordarray_map_no_break (ArrayMapP.make arr frm to body acc obs))"
  and wordarray_cmp_ret:
  "\<And>P. P(\<alpha>wa a1 = \<alpha>wa a2) \<Longrightarrow> P (wordarray_cmp(a1, a2))"
  and wordarray_set_ret:
  "(offs::U32) \<le> offs + len \<Longrightarrow>
   wordarray_set (wa, offs, len, (v::U8)) =
   WordArrayT.make ((take (unat offs) (\<alpha>wa wa) @
                   replicate (unat len) v @ drop (unat (offs + len)) (\<alpha>wa wa)))"

  and wordarray_copy_ret:
  "\<And>P. \<lbrakk>  length (\<alpha>wa dst) = length (\<alpha>wa src) \<Longrightarrow>
                  offs = src_offs \<Longrightarrow>
                  offs \<le> offs + len \<Longrightarrow>
                  unat (offs + len) \<le> length (\<alpha>wa src) \<Longrightarrow>
         P (WordArrayT.make (take (unat offs) (\<alpha>wa dst) @ slice (unat offs) (unat offs + unat len) (\<alpha>wa src) @ drop (unat (offs+len)) (\<alpha>wa dst))) \<rbrakk>
     \<Longrightarrow>
      P (wordarray_copy(dst, src, offs, src_offs, len))"

lemma wordarray_\<alpha>wa_eq:
  "\<And>xs ys. (xs = ys) \<longleftrightarrow> \<alpha>wa xs = \<alpha>wa ys"
  apply (rule iffI)
   apply (erule arg_cong[where f=\<alpha>wa])
   apply (drule_tac x="\<alpha>wa xs" and y="\<alpha>wa ys" in arg_cong[where f=WordArrayT.make])
  apply (simp add: wordarray_make')
done

lemma ElemA_ext_inject_plus:
  "(\<lparr>ElemA.elem\<^sub>f = a, ElemA.acc\<^sub>f = b\<rparr> = v) = (ElemA.elem\<^sub>f v = a \<and> ElemA.acc\<^sub>f v = b)"
  by (case_tac v, auto)

lemma wordarray_modify_length':
  "\<And>index modifier vacc obs wa. unat index < length (\<alpha>wa wa) \<Longrightarrow>
   (length $ \<alpha>wa $ ArrA.arr\<^sub>f $ wordarray_modify (ArrayUseValueP.make wa index modifier vacc obs)) = (length $ \<alpha>wa $ wa)"
  by (fastforce intro: wordarray_modify_ret
                 simp: ArrA.make_def wordarray_make ElemA_ext_inject_plus
                       ElemA.make_def ElemAO.make_def)+

lemma wordarray_modify_length:
  "\<And>index modifier vacc obs wa. unat index < length (\<alpha>wa wa) \<Longrightarrow>
  P (length $ \<alpha>wa $ wa) \<Longrightarrow>
   P(length (\<alpha>wa (ArrA.arr\<^sub>f ( wordarray_modify (ArrayUseValueP.make wa index modifier vacc obs)))))"
   by (fastforce simp: wordarray_modify_length'[simplified])

lemma wordarray_get_ret':
  "\<lbrakk> unat index < length (\<alpha>wa arr); P (\<alpha>wa arr ! unat index) \<rbrakk> \<Longrightarrow>
    P (wordarray_get (arr, index))"
    using wordarray_get_ret by fastforce

lemma wordarray_length_ofnat:
  "unat (wordarray_length wa) = length (\<alpha>wa wa) \<Longrightarrow>
  wordarray_length wa = of_nat (length (\<alpha>wa wa))"
  by (drule sym, simp)

lemmas wordarray_make_rev = wordarray_make'

end

author: au-ts

repo: cogent

save_path: github-repos/isabelle/au-ts-cogent