<commit_before>(*  Title: 	ZF/IMP/Equiv.ML
    ID:         $Id$
    Author: 	<NAME> & <NAME>, TUM
    Copyright   1994 TUM
*)

val prems = goal Equiv.thy "[| a: aexp; sigma: loc -> nat |] ==> \
\ <a,sigma> -a-> n <-> A(a,sigma) = n";
by (res_inst_tac [("x","n")] spec 1);                       (* quantify n *)
by (res_inst_tac [("x","a")] aexp.induct 1);                (* struct. ind. *)
by (resolve_tac prems 1);                                   (* type prem. *)
by (rewrite_goals_tac A_rewrite_rules);			    (* rewr. Den.   *)
by (TRYALL (fast_tac (ZF_cs addSIs (evala.intrs@prems)
                            addSEs aexp_elim_cases)));
val aexp_iff = result();


val aexp1 = prove_goal Equiv.thy
        "[| <a,sigma> -a-> n; a: aexp; sigma: loc -> nat |] \
        \ ==> A(a,sigma) = n"	    (* destruction rule *)
     (fn prems => [(fast_tac (ZF_cs addSIs ((aexp_iff RS iffD1)::prems)) 1)]);
val aexp2 = aexp_iff RS iffD2;


val bexp_elim_cases = 
   [
    evalb.mk_cases bexp.con_defs "<true,sigma> -b-> x",
    evalb.mk_cases bexp.con_defs "<false,sigma> -b-> x",
    evalb.mk_cases bexp.con_defs "<ROp(f,a0,a1),sigma> -b-> x",
    evalb.mk_cases bexp.con_defs "<noti(b),sigma> -b-> x",
    evalb.mk_cases bexp.con_defs "<b0 andi b1,sigma> -b-> x",
    evalb.mk_cases bexp.con_defs "<b0 ori b1,sigma> -b-> x"
   ];


val prems = goal Equiv.thy "[| b: bexp; sigma: loc -> nat |] ==> \
\ <b,sigma> -b-> w <-> B(b,sigma) = w";
by (res_inst_tac [("x","w")] spec 1);			(* quantify w *)
by (res_inst_tac [("x","b")] bexp.induct 1);		(* struct. ind. *)
by (resolve_tac prems 1);				(* type prem. *)
by (rewrite_goals_tac B_rewrite_rules);			(* rewr. Den.   *)
by (TRYALL (fast_tac (ZF_cs addSIs (evalb.intrs@prems@[aexp2])
                            addSDs [aexp1] addSEs bexp_elim_cases)));
val bexp_iff = result();

val bexp1 = prove_goal Equiv.thy
        "[| <b,sigma> -b-> w; b: bexp; sigma: loc -> nat |]\
        \ ==> B(b,sigma) = w"
     (fn prems => [(fast_tac (ZF_cs addSIs ((bexp_iff RS iffD1)::prems)) 1)]);
val bexp2 = bexp_iff RS iffD2;

goal Equiv.thy "!!c. <c,sigma> -c-> sigma' ==> <sigma,sigma'> : C(c)";

(* start with rule induction *)
be (evalc.mutual_induct RS spec RS spec RS spec RSN (2,rev_mp)) 1;

by (rewrite_tac (Gamma_def::C_rewrite_rules));
(* skip *)
by (fast_tac comp_cs 1);

(* assign *)
by (asm_full_simp_tac (ZF_ss addsimps [aexp1,assign_type] @
                                      op_type_intrs) 1);
(* comp *)
by (fast_tac comp_cs 1);

(* if *)
by (fast_tac (ZF_cs addSIs [bexp1] addIs  [(fst_conv RS ssubst)]) 1);
by (fast_tac (ZF_cs addSIs [bexp1] addIs  [(fst_conv RS ssubst)]) 1);

(* while *)
by (etac (rewrite_rule [Gamma_def] (Gamma_bnd_mono RS lfp_Tarski RS ssubst)) 1);
by (fast_tac (comp_cs addSIs [bexp1,idI]@evalb_type_intrs
                      addIs  [(fst_conv RS ssubst)]) 1);

by (etac (rewrite_rule [Gamma_def] (Gamma_bnd_mono RS lfp_Tarski RS ssubst)) 1);
by (fast_tac (comp_cs addSIs [bexp1,compI]@evalb_type_intrs
                      addIs  [(fst_conv RS ssubst)]) 1);

val com1 = result();


val com_cs = ZF_cs addSIs [aexp2,bexp2,B_type,A_type]
                   addIs evalc.intrs
                   addSEs [idE,compE]
                   addEs [C_type,C_type_fst];

val [prem] = goal Equiv.thy
    "c : com ==> ALL x:C(c). <c,fst(x)> -c-> snd(x)";
br (prem RS com.induct) 1;
by (rewrite_tac C_rewrite_rules);
by (safe_tac com_cs);
by (ALLGOALS (asm_full_simp_tac ZF_ss));

(* skip *)
by (fast_tac com_cs 1);

(* assign *)
by (fast_tac com_cs 1);

(* comp *)
by (REPEAT (EVERY [(dtac bspec 1),(atac 1)]));
by (asm_full_simp_tac ZF_ss 1);<commit_msg>com1,2: added simplifier calls to remove use of ssubst in fast_tac<commit_after>(*  Title: 	ZF/IMP/Equiv.ML
    ID:         $Id$
    Author: 	<NAME> & <NAME>, TUM
    Copyright   1994 TUM
*)

val prems = goal Equiv.thy "[| a: aexp; sigma: loc -> nat |] ==> \
\ <a,sigma> -a-> n <-> A(a,sigma) = n";
by (res_inst_tac [("x","n")] spec 1);                       (* quantify n *)
by (res_inst_tac [("x","a")] aexp.induct 1);                (* struct. ind. *)
by (resolve_tac prems 1);                                   (* type prem. *)
by (rewrite_goals_tac A_rewrite_rules);			    (* rewr. Den.   *)
by (TRYALL (fast_tac (ZF_cs addSIs (evala.intrs@prems)
                            addSEs aexp_elim_cases)));
val aexp_iff = result();


val aexp1 = prove_goal Equiv.thy
        "[| <a,sigma> -a-> n; a: aexp; sigma: loc -> nat |] \
        \ ==> A(a,sigma) = n"	    (* destruction rule *)
     (fn prems => [(fast_tac (ZF_cs addSIs ((aexp_iff RS iffD1)::prems)) 1)]);
val aexp2 = aexp_iff RS iffD2;


val bexp_elim_cases = 
   [
    evalb.mk_cases bexp.con_defs "<true,sigma> -b-> x",
    evalb.mk_cases bexp.con_defs "<false,sigma> -b-> x",
    evalb.mk_cases bexp.con_defs "<ROp(f,a0,a1),sigma> -b-> x",
    evalb.mk_cases bexp.con_defs "<noti(b),sigma> -b-> x",
    evalb.mk_cases bexp.con_defs "<b0 andi b1,sigma> -b-> x",
    evalb.mk_cases bexp.con_defs "<b0 ori b1,sigma> -b-> x"
   ];


val prems = goal Equiv.thy "[| b: bexp; sigma: loc -> nat |] ==> \
\ <b,sigma> -b-> w <-> B(b,sigma) = w";
by (res_inst_tac [("x","w")] spec 1);			(* quantify w *)
by (res_inst_tac [("x","b")] bexp.induct 1);		(* struct. ind. *)
by (resolve_tac prems 1);				(* type prem. *)
by (rewrite_goals_tac B_rewrite_rules);			(* rewr. Den.   *)
by (TRYALL (fast_tac (ZF_cs addSIs (evalb.intrs@prems@[aexp2])
                            addSDs [aexp1] addSEs bexp_elim_cases)));
val bexp_iff = result();

val bexp1 = prove_goal Equiv.thy
        "[| <b,sigma> -b-> w; b: bexp; sigma: loc -> nat |]\
        \ ==> B(b,sigma) = w"
     (fn prems => [(fast_tac (ZF_cs addSIs ((bexp_iff RS iffD1)::prems)) 1)]);
val bexp2 = bexp_iff RS iffD2;

goal Equiv.thy "!!c. <c,sigma> -c-> sigma' ==> <sigma,sigma'> : C(c)";

(* start with rule induction *)
be (evalc.mutual_induct RS spec RS spec RS spec RSN (2,rev_mp)) 1;

by (rewrite_tac (Gamma_def::C_rewrite_rules));
(* skip *)
by (fast_tac comp_cs 1);

(* assign *)
by (asm_full_simp_tac (ZF_ss addsimps [aexp1,assign_type] @ op_type_intrs) 1);

(* comp *)
by (fast_tac comp_cs 1);

(* if *)
by (asm_simp_tac (ZF_ss addsimps [bexp1]) 1);
by (asm_simp_tac (ZF_ss addsimps [bexp1]) 1);

(* while *)
by (etac (rewrite_rule [Gamma_def]
	  (Gamma_bnd_mono RS lfp_Tarski RS ssubst)) 1);
by (asm_simp_tac (ZF_ss addsimps [bexp1]) 1);
by (fast_tac (comp_cs addSIs [bexp1,idI]@evalb_type_intrs) 1);

by (etac (rewrite_rule [Gamma_def]
	  (Gamma_bnd_mono RS lfp_Tarski RS ssubst)) 1);
by (asm_simp_tac (ZF_ss addsimps [bexp1]) 1);
by (fast_tac (comp_cs addSIs [bexp1,compI]@evalb_type_intrs) 1);

val com1 = result();


val com_cs = ZF_cs addSIs [aexp2,bexp2,B_type,A_type]
                   addIs evalc.intrs
                   addSEs [idE,compE]
                   addEs [C_type,C_type_fst];

val [prem] = goal Equiv.thy
    "c : com ==> ALL x:C(c). <c,fst(x)> -c-> snd(x)";
br (prem RS com.induct) 1;
by (rewrite_tac C_rewrite_rules);
by (safe_tac com_cs);
by (ALLGOALS (asm_full_simp_tac ZF_ss));

(* skip *)
by (fast_tac com_cs 1);

(* assign *)
by (fast_tac com_cs 1);

(* comp *)
by (REPEAT (EVERY [(dtac bspec 1),(atac 1)]));
by (asm_full_simp_tac ZF_ss 1);
{'fraction_non_alphanumeric': 0.17583333333333334, 'fraction_numerical': 0.015555555555555555, 'mean_word_length': 2.909337676438654, 'pattern_counts': {'":': 0, '<': 37, '<?xml version=': 0, '>': 85, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 5, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '4697158', 'n_tokens_mistral': 3290, 'n_tokens_neox': 3128, 'n_words': 757}