Old_HOL: IMP/Equiv.ML@32b84b520cd3 (annotated)

132 47be9d22a0d6 Renamed a few types and vars nipkow parents: 131 diff changeset	1	(* Title: HOL/IMP/Equiv.ML
131 41bf53133ba6 Equivalence of op. and den. sem. for simple while language. nipkow parents: diff changeset	2	ID: $Id$
41bf53133ba6 Equivalence of op. and den. sem. for simple while language. nipkow parents: diff changeset	3	Author: Heiko Loetzbeyer & Robert Sandner, TUM
41bf53133ba6 Equivalence of op. and den. sem. for simple while language. nipkow parents: diff changeset	4	Copyright 1994 TUM
41bf53133ba6 Equivalence of op. and den. sem. for simple while language. nipkow parents: diff changeset	5	*)
41bf53133ba6 Equivalence of op. and den. sem. for simple while language. nipkow parents: diff changeset	6
158 7c537d03f875 Replaced fast_tac by simp_tac in a number of places. nipkow parents: 139 diff changeset	7	goal Equiv.thy "!n. (<a,s> -a-> n) = (n = A(a,s))";
131 41bf53133ba6 Equivalence of op. and den. sem. for simple while language. nipkow parents: diff changeset	8	by (aexp.induct_tac "a" 1); (* struct. ind. *)
137 bca8203b0e91 Converted rules to primrecs nipkow parents: 132 diff changeset	9	by (ALLGOALS(simp_tac (HOL_ss addsimps A_simps))); (* rewr. Den. *)
131 41bf53133ba6 Equivalence of op. and den. sem. for simple while language. nipkow parents: diff changeset	10	by (TRYALL (fast_tac (set_cs addSIs (evala.intrs@prems)
158 7c537d03f875 Replaced fast_tac by simp_tac in a number of places. nipkow parents: 139 diff changeset	11	addSEs evala_elim_cases)));
171 16c4ea954511 replaced 'val ... = result()' by 'qed "..."' clasohm parents: 158 diff changeset	12	val aexp_iff = store_thm("aexp_iff", result() RS spec);
131 41bf53133ba6 Equivalence of op. and den. sem. for simple while language. nipkow parents: diff changeset	13
41bf53133ba6 Equivalence of op. and den. sem. for simple while language. nipkow parents: diff changeset	14
158 7c537d03f875 Replaced fast_tac by simp_tac in a number of places. nipkow parents: 139 diff changeset	15	goal HOL.thy "(? x. x=t & P) = P";
7c537d03f875 Replaced fast_tac by simp_tac in a number of places. nipkow parents: 139 diff changeset	16	by(fast_tac HOL_cs 1);
171 16c4ea954511 replaced 'val ... = result()' by 'qed "..."' clasohm parents: 158 diff changeset	17	qed "elim_ex_conv";
139 96c68fd7ed46 HOL/IMP/Equiv/bexp_iff: split proof into separate directions, to be faster lcp parents: 137 diff changeset	18
158 7c537d03f875 Replaced fast_tac by simp_tac in a number of places. nipkow parents: 139 diff changeset	19	goal Equiv.thy "!w. (<b,s> -b-> w) = (w = B(b,s))";
139 96c68fd7ed46 HOL/IMP/Equiv/bexp_iff: split proof into separate directions, to be faster lcp parents: 137 diff changeset	20	by (bexp.induct_tac "b" 1);
158 7c537d03f875 Replaced fast_tac by simp_tac in a number of places. nipkow parents: 139 diff changeset	21	by (ALLGOALS(asm_simp_tac (HOL_ss addcongs [conj_cong]
7c537d03f875 Replaced fast_tac by simp_tac in a number of places. nipkow parents: 139 diff changeset	22	addsimps (aexp_iff::elim_ex_conv::B_simps@evalb_simps))));
171 16c4ea954511 replaced 'val ... = result()' by 'qed "..."' clasohm parents: 158 diff changeset	23	val bexp_iff = store_thm("bexp_iff", result() RS spec);
139 96c68fd7ed46 HOL/IMP/Equiv/bexp_iff: split proof into separate directions, to be faster lcp parents: 137 diff changeset	24
158 7c537d03f875 Replaced fast_tac by simp_tac in a number of places. nipkow parents: 139 diff changeset	25	val bexp1 = bexp_iff RS iffD1;
7c537d03f875 Replaced fast_tac by simp_tac in a number of places. nipkow parents: 139 diff changeset	26	val bexp2 = bexp_iff RS iffD2;
131 41bf53133ba6 Equivalence of op. and den. sem. for simple while language. nipkow parents: diff changeset	27
41bf53133ba6 Equivalence of op. and den. sem. for simple while language. nipkow parents: diff changeset	28	val BfstI = read_instantiate_sg (sign_of Equiv.thy)
41bf53133ba6 Equivalence of op. and den. sem. for simple while language. nipkow parents: diff changeset	29	[("P","%x.B(?b,x)")] (fst_conv RS ssubst);
41bf53133ba6 Equivalence of op. and den. sem. for simple while language. nipkow parents: diff changeset	30	val BfstD = read_instantiate_sg (sign_of Equiv.thy)
41bf53133ba6 Equivalence of op. and den. sem. for simple while language. nipkow parents: diff changeset	31	[("P","%x.B(?b,x)")] (fst_conv RS subst);
41bf53133ba6 Equivalence of op. and den. sem. for simple while language. nipkow parents: diff changeset	32
132 47be9d22a0d6 Renamed a few types and vars nipkow parents: 131 diff changeset	33	goal Equiv.thy "!!c. <c,s> -c-> t ==> <s,t> : C(c)";
131 41bf53133ba6 Equivalence of op. and den. sem. for simple while language. nipkow parents: diff changeset	34
41bf53133ba6 Equivalence of op. and den. sem. for simple while language. nipkow parents: diff changeset	35	(* start with rule induction *)
41bf53133ba6 Equivalence of op. and den. sem. for simple while language. nipkow parents: diff changeset	36	be (evalc.mutual_induct RS spec RS spec RS spec RSN (2,rev_mp)) 1;
137 bca8203b0e91 Converted rules to primrecs nipkow parents: 132 diff changeset	37	by (rewrite_tac (Gamma_def::C_simps));
bca8203b0e91 Converted rules to primrecs nipkow parents: 132 diff changeset	38	(* simplification with HOL_ss again too agressive *)
131 41bf53133ba6 Equivalence of op. and den. sem. for simple while language. nipkow parents: diff changeset	39	(* skip *)
41bf53133ba6 Equivalence of op. and den. sem. for simple while language. nipkow parents: diff changeset	40	by (fast_tac comp_cs 1);
41bf53133ba6 Equivalence of op. and den. sem. for simple while language. nipkow parents: diff changeset	41	(* assign *)
158 7c537d03f875 Replaced fast_tac by simp_tac in a number of places. nipkow parents: 139 diff changeset	42	by (asm_full_simp_tac (prod_ss addsimps [aexp_iff]) 1);
131 41bf53133ba6 Equivalence of op. and den. sem. for simple while language. nipkow parents: diff changeset	43	(* comp *)
41bf53133ba6 Equivalence of op. and den. sem. for simple while language. nipkow parents: diff changeset	44	by (fast_tac comp_cs 1);
41bf53133ba6 Equivalence of op. and den. sem. for simple while language. nipkow parents: diff changeset	45	(* if *)
41bf53133ba6 Equivalence of op. and den. sem. for simple while language. nipkow parents: diff changeset	46	by(fast_tac (set_cs addSIs [BfstI] addSDs [BfstD,bexp1]) 1);
41bf53133ba6 Equivalence of op. and den. sem. for simple while language. nipkow parents: diff changeset	47	by(fast_tac (set_cs addSIs [BfstI] addSDs [BfstD,bexp1]) 1);
41bf53133ba6 Equivalence of op. and den. sem. for simple while language. nipkow parents: diff changeset	48	(* while *)
41bf53133ba6 Equivalence of op. and den. sem. for simple while language. nipkow parents: diff changeset	49	by (rtac (rewrite_rule [Gamma_def] (Gamma_mono RS lfp_Tarski RS ssubst)) 1);
41bf53133ba6 Equivalence of op. and den. sem. for simple while language. nipkow parents: diff changeset	50	by (fast_tac (comp_cs addSIs [bexp1,BfstI] addSDs [BfstD,bexp1]) 1);
41bf53133ba6 Equivalence of op. and den. sem. for simple while language. nipkow parents: diff changeset	51	by (rtac (rewrite_rule [Gamma_def] (Gamma_mono RS lfp_Tarski RS ssubst)) 1);
41bf53133ba6 Equivalence of op. and den. sem. for simple while language. nipkow parents: diff changeset	52	by (fast_tac (comp_cs addSIs [bexp1,BfstI] addSDs [BfstD,bexp1]) 1);
41bf53133ba6 Equivalence of op. and den. sem. for simple while language. nipkow parents: diff changeset	53
171 16c4ea954511 replaced 'val ... = result()' by 'qed "..."' clasohm parents: 158 diff changeset	54	qed "com1";
131 41bf53133ba6 Equivalence of op. and den. sem. for simple while language. nipkow parents: diff changeset	55
41bf53133ba6 Equivalence of op. and den. sem. for simple while language. nipkow parents: diff changeset	56
158 7c537d03f875 Replaced fast_tac by simp_tac in a number of places. nipkow parents: 139 diff changeset	57	val com_ss = prod_ss addsimps (aexp_iff::bexp_iff::evalc.intrs);
131 41bf53133ba6 Equivalence of op. and den. sem. for simple while language. nipkow parents: diff changeset	58
132 47be9d22a0d6 Renamed a few types and vars nipkow parents: 131 diff changeset	59	goal Equiv.thy "!io:C(c). <c,fst(io)> -c-> snd(io)";
131 41bf53133ba6 Equivalence of op. and den. sem. for simple while language. nipkow parents: diff changeset	60	by (com.induct_tac "c" 1);
137 bca8203b0e91 Converted rules to primrecs nipkow parents: 132 diff changeset	61	by (rewrite_tac C_simps);
158 7c537d03f875 Replaced fast_tac by simp_tac in a number of places. nipkow parents: 139 diff changeset	62	by (safe_tac comp_cs);
7c537d03f875 Replaced fast_tac by simp_tac in a number of places. nipkow parents: 139 diff changeset	63	by (ALLGOALS (asm_full_simp_tac com_ss));
131 41bf53133ba6 Equivalence of op. and den. sem. for simple while language. nipkow parents: diff changeset	64
41bf53133ba6 Equivalence of op. and den. sem. for simple while language. nipkow parents: diff changeset	65	(* comp *)
41bf53133ba6 Equivalence of op. and den. sem. for simple while language. nipkow parents: diff changeset	66	by (REPEAT (EVERY [(dtac bspec 1),(atac 1)]));
158 7c537d03f875 Replaced fast_tac by simp_tac in a number of places. nipkow parents: 139 diff changeset	67	by (asm_full_simp_tac com_ss 1);
131 41bf53133ba6 Equivalence of op. and den. sem. for simple while language. nipkow parents: diff changeset	68
41bf53133ba6 Equivalence of op. and den. sem. for simple while language. nipkow parents: diff changeset	69	(* while *)
41bf53133ba6 Equivalence of op. and den. sem. for simple while language. nipkow parents: diff changeset	70	by (etac (Gamma_mono RSN (2,induct)) 1);
41bf53133ba6 Equivalence of op. and den. sem. for simple while language. nipkow parents: diff changeset	71	by (rewrite_goals_tac [Gamma_def]);
158 7c537d03f875 Replaced fast_tac by simp_tac in a number of places. nipkow parents: 139 diff changeset	72	by (safe_tac comp_cs);
131 41bf53133ba6 Equivalence of op. and den. sem. for simple while language. nipkow parents: diff changeset	73	by (EVERY1 [dtac bspec, atac]);
158 7c537d03f875 Replaced fast_tac by simp_tac in a number of places. nipkow parents: 139 diff changeset	74	by (ALLGOALS (asm_full_simp_tac com_ss));
131 41bf53133ba6 Equivalence of op. and den. sem. for simple while language. nipkow parents: diff changeset	75
171 16c4ea954511 replaced 'val ... = result()' by 'qed "..."' clasohm parents: 158 diff changeset	76	qed "com2";
131 41bf53133ba6 Equivalence of op. and den. sem. for simple while language. nipkow parents: diff changeset	77
41bf53133ba6 Equivalence of op. and den. sem. for simple while language. nipkow parents: diff changeset	78
41bf53133ba6 Equivalence of op. and den. sem. for simple while language. nipkow parents: diff changeset	79	(** Proof of Equivalence **)
41bf53133ba6 Equivalence of op. and den. sem. for simple while language. nipkow parents: diff changeset	80
158 7c537d03f875 Replaced fast_tac by simp_tac in a number of places. nipkow parents: 139 diff changeset	81	val com_iff_cs = set_cs addEs [com2 RS bspec] addDs [com1];
131 41bf53133ba6 Equivalence of op. and den. sem. for simple while language. nipkow parents: diff changeset	82
41bf53133ba6 Equivalence of op. and den. sem. for simple while language. nipkow parents: diff changeset	83	goal Equiv.thy "C(c) = {io . <c,fst(io)> -c-> snd(io)}";
41bf53133ba6 Equivalence of op. and den. sem. for simple while language. nipkow parents: diff changeset	84	by (rtac equalityI 1);
41bf53133ba6 Equivalence of op. and den. sem. for simple while language. nipkow parents: diff changeset	85	(* => *)
41bf53133ba6 Equivalence of op. and den. sem. for simple while language. nipkow parents: diff changeset	86	by (fast_tac com_iff_cs 1);
41bf53133ba6 Equivalence of op. and den. sem. for simple while language. nipkow parents: diff changeset	87	(* <= *)
41bf53133ba6 Equivalence of op. and den. sem. for simple while language. nipkow parents: diff changeset	88	by (REPEAT (step_tac com_iff_cs 1));
41bf53133ba6 Equivalence of op. and den. sem. for simple while language. nipkow parents: diff changeset	89	by (asm_full_simp_tac (prod_ss addsimps [surjective_pairing RS sym])1);
171 16c4ea954511 replaced 'val ... = result()' by 'qed "..."' clasohm parents: 158 diff changeset	90	qed "com_equivalence";

author	nipkow
	Fri, 25 Nov 1994 20:06:15 +0100
changeset 188	32b84b520cd3
parent 171	16c4ea954511
child 197	2757544bbe6d
permissions	-rw-r--r--