author | nipkow |
Tue, 14 Mar 1995 09:47:28 +0100 | |
changeset 951 | 682139612060 |
parent 924 | 806721cfbf46 |
child 972 | e61b058d58d2 |
permissions | -rw-r--r-- |
924
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
1 |
(* Title: HOL/IMP/Equiv.ML |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
2 |
ID: $Id$ |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
3 |
Author: Heiko Loetzbeyer & Robert Sandner, TUM |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
4 |
Copyright 1994 TUM |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
5 |
*) |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
6 |
|
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
7 |
goal Equiv.thy "!n. (<a,s> -a-> n) = (n = A a s)"; |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
8 |
by (aexp.induct_tac "a" 1); (* struct. ind. *) |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
9 |
by (ALLGOALS(simp_tac (HOL_ss addsimps A_simps))); (* rewr. Den. *) |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
10 |
by (TRYALL (fast_tac (set_cs addSIs (evala.intrs@prems) |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
11 |
addSEs evala_elim_cases))); |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
12 |
bind_thm("aexp_iff", result() RS spec); |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
13 |
|
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
14 |
goal Equiv.thy "!w. (<b,s> -b-> w) = (w = B b s)"; |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
15 |
by (bexp.induct_tac "b" 1); |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
16 |
by (ALLGOALS(asm_simp_tac (HOL_ss addcongs [conj_cong] |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
17 |
addsimps (aexp_iff::B_simps@evalb_simps)))); |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
18 |
bind_thm("bexp_iff", result() RS spec); |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
19 |
|
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
20 |
val bexp1 = bexp_iff RS iffD1; |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
21 |
val bexp2 = bexp_iff RS iffD2; |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
22 |
|
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
23 |
val BfstI = read_instantiate_sg (sign_of Equiv.thy) |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
24 |
[("P","%x.B ?b x")] (fst_conv RS ssubst); |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
25 |
val BfstD = read_instantiate_sg (sign_of Equiv.thy) |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
26 |
[("P","%x.B ?b x")] (fst_conv RS subst); |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
27 |
|
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
28 |
goal Equiv.thy "!!c. <c,s> -c-> t ==> <s,t> : C(c)"; |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
29 |
|
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
30 |
(* start with rule induction *) |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
31 |
be (evalc.mutual_induct RS spec RS spec RS spec RSN (2,rev_mp)) 1; |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
32 |
by (rewrite_tac (Gamma_def::C_simps)); |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
33 |
(* simplification with HOL_ss again too agressive *) |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
34 |
(* skip *) |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
35 |
by (fast_tac comp_cs 1); |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
36 |
(* assign *) |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
37 |
by (asm_full_simp_tac (prod_ss addsimps [aexp_iff]) 1); |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
38 |
(* comp *) |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
39 |
by (fast_tac comp_cs 1); |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
40 |
(* if *) |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
41 |
by(fast_tac (set_cs addSIs [BfstI] addSDs [BfstD,bexp1]) 1); |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
42 |
by(fast_tac (set_cs addSIs [BfstI] addSDs [BfstD,bexp1]) 1); |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
43 |
(* while *) |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
44 |
by (rtac (rewrite_rule [Gamma_def] (Gamma_mono RS lfp_Tarski RS ssubst)) 1); |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
45 |
by (fast_tac (comp_cs addSIs [bexp1,BfstI] addSDs [BfstD,bexp1]) 1); |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
46 |
by (rtac (rewrite_rule [Gamma_def] (Gamma_mono RS lfp_Tarski RS ssubst)) 1); |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
47 |
by (fast_tac (comp_cs addSIs [bexp1,BfstI] addSDs [BfstD,bexp1]) 1); |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
48 |
|
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
49 |
qed "com1"; |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
50 |
|
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
51 |
|
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
52 |
val com_ss = prod_ss addsimps (aexp_iff::bexp_iff::evalc.intrs); |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
53 |
|
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
54 |
goal Equiv.thy "!io:C(c). <c,fst(io)> -c-> snd(io)"; |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
55 |
by (com.induct_tac "c" 1); |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
56 |
by (rewrite_tac C_simps); |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
57 |
by (safe_tac comp_cs); |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
58 |
by (ALLGOALS (asm_full_simp_tac com_ss)); |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
59 |
|
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
60 |
(* comp *) |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
61 |
by (REPEAT (EVERY [(dtac bspec 1),(atac 1)])); |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
62 |
by (asm_full_simp_tac com_ss 1); |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
63 |
|
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
64 |
(* while *) |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
65 |
by (etac (Gamma_mono RSN (2,induct)) 1); |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
66 |
by (rewrite_goals_tac [Gamma_def]); |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
67 |
by (safe_tac comp_cs); |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
68 |
by (EVERY1 [dtac bspec, atac]); |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
69 |
by (ALLGOALS (asm_full_simp_tac com_ss)); |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
70 |
|
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
71 |
qed "com2"; |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
72 |
|
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
73 |
|
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
74 |
(**** Proof of Equivalence ****) |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
75 |
|
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
76 |
val com_iff_cs = set_cs addEs [com2 RS bspec] addDs [com1]; |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
77 |
|
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
78 |
goal Equiv.thy "C(c) = {io . <c,fst(io)> -c-> snd(io)}"; |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
79 |
by (rtac equalityI 1); |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
80 |
(* => *) |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
81 |
by (fast_tac com_iff_cs 1); |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
82 |
(* <= *) |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
83 |
by (REPEAT (step_tac com_iff_cs 1)); |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
84 |
by (asm_full_simp_tac (prod_ss addsimps [surjective_pairing RS sym])1); |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
85 |
qed "com_equivalence"; |