7 open PER0; |
7 open PER0; |
8 |
8 |
9 (* derive the characteristic axioms *) |
9 (* derive the characteristic axioms *) |
10 val prems = goalw thy [per_def] "x === y ==> y === x"; |
10 val prems = goalw thy [per_def] "x === y ==> y === x"; |
11 by (cut_facts_tac prems 1); |
11 by (cut_facts_tac prems 1); |
12 be ax_per_sym 1; |
12 by (etac ax_per_sym 1); |
13 qed "per_sym"; |
13 qed "per_sym"; |
14 |
14 |
15 val prems = goalw thy [per_def] "[| x === y; y === z |] ==> x === z"; |
15 val prems = goalw thy [per_def] "[| x === y; y === z |] ==> x === z"; |
16 by (cut_facts_tac prems 1); |
16 by (cut_facts_tac prems 1); |
17 be ax_per_trans 1; |
17 by (etac ax_per_trans 1); |
18 ba 1; |
18 by (assume_tac 1); |
19 qed "per_trans"; |
19 qed "per_trans"; |
20 |
20 |
21 goalw thy [per_def] "(x::'a::er) === x"; |
21 goalw thy [per_def] "(x::'a::er) === x"; |
22 br ax_er_refl 1; |
22 by (rtac ax_er_refl 1); |
23 qed "er_refl"; |
23 qed "er_refl"; |
24 |
24 |
25 (* now everything works without axclasses *) |
25 (* now everything works without axclasses *) |
26 |
26 |
27 goal thy "x===y=y===x"; |
27 goal thy "x===y=y===x"; |
28 br iffI 1; |
28 by (rtac iffI 1); |
29 be per_sym 1; |
29 by (etac per_sym 1); |
30 be per_sym 1; |
30 by (etac per_sym 1); |
31 qed "per_sym2"; |
31 qed "per_sym2"; |
32 |
32 |
33 val prems = goal thy "x===y ==> x===x"; |
33 val prems = goal thy "x===y ==> x===x"; |
34 by (cut_facts_tac prems 1); |
34 by (cut_facts_tac prems 1); |
35 br per_trans 1;ba 1; |
35 by (rtac per_trans 1);by (assume_tac 1); |
36 be per_sym 1; |
36 by (etac per_sym 1); |
37 qed "sym2refl1"; |
37 qed "sym2refl1"; |
38 |
38 |
39 val prems = goal thy "x===y ==> y===y"; |
39 val prems = goal thy "x===y ==> y===y"; |
40 by (cut_facts_tac prems 1); |
40 by (cut_facts_tac prems 1); |
41 br per_trans 1;ba 2; |
41 by (rtac per_trans 1);by (assume_tac 2); |
42 be per_sym 1; |
42 by (etac per_sym 1); |
43 qed "sym2refl2"; |
43 qed "sym2refl2"; |
44 |
44 |
45 val prems = goalw thy [Dom] "x:D ==> x === x"; |
45 val prems = goalw thy [Dom] "x:D ==> x === x"; |
46 by (cut_facts_tac prems 1); |
46 by (cut_facts_tac prems 1); |
47 by (fast_tac set_cs 1); |
47 by (fast_tac set_cs 1); |
51 by (cut_facts_tac prems 1); |
51 by (cut_facts_tac prems 1); |
52 by (fast_tac set_cs 1); |
52 by (fast_tac set_cs 1); |
53 qed "DomainI"; |
53 qed "DomainI"; |
54 |
54 |
55 goal thy "x:D = x===x"; |
55 goal thy "x:D = x===x"; |
56 br iffI 1; |
56 by (rtac iffI 1); |
57 be DomainD 1; |
57 by (etac DomainD 1); |
58 be DomainI 1; |
58 by (etac DomainI 1); |
59 qed "DomainEq"; |
59 qed "DomainEq"; |
60 |
60 |
61 goal thy "(~ x === y) = (~ y === x)"; |
61 goal thy "(~ x === y) = (~ y === x)"; |
62 br (per_sym2 RS arg_cong) 1; |
62 by (rtac (per_sym2 RS arg_cong) 1); |
63 qed "per_not_sym"; |
63 qed "per_not_sym"; |
64 |
64 |
65 (* show that PER work only on D *) |
65 (* show that PER work only on D *) |
66 val prems = goal thy "x===y ==> x:D"; |
66 val prems = goal thy "x===y ==> x:D"; |
67 by (cut_facts_tac prems 1); |
67 by (cut_facts_tac prems 1); |
68 be (sym2refl1 RS DomainI) 1; |
68 by (etac (sym2refl1 RS DomainI) 1); |
69 qed "DomainI_left"; |
69 qed "DomainI_left"; |
70 |
70 |
71 val prems = goal thy "x===y ==> y:D"; |
71 val prems = goal thy "x===y ==> y:D"; |
72 by (cut_facts_tac prems 1); |
72 by (cut_facts_tac prems 1); |
73 be (sym2refl2 RS DomainI) 1; |
73 by (etac (sym2refl2 RS DomainI) 1); |
74 qed "DomainI_right"; |
74 qed "DomainI_right"; |
75 |
75 |
76 val prems = goalw thy [Dom] "x~:D ==> ~x===y"; |
76 val prems = goalw thy [Dom] "x~:D ==> ~x===y"; |
77 by (cut_facts_tac prems 1); |
77 by (cut_facts_tac prems 1); |
78 by (res_inst_tac [("Q","x===y")] (excluded_middle RS disjE) 1);ba 1; |
78 by (res_inst_tac [("Q","x===y")] (excluded_middle RS disjE) 1);by (assume_tac 1); |
79 bd sym2refl1 1; |
79 by (dtac sym2refl1 1); |
80 by (fast_tac set_cs 1); |
80 by (fast_tac set_cs 1); |
81 qed "notDomainE1"; |
81 qed "notDomainE1"; |
82 |
82 |
83 val prems = goalw thy [Dom] "x~:D ==> ~y===x"; |
83 val prems = goalw thy [Dom] "x~:D ==> ~y===x"; |
84 by (cut_facts_tac prems 1); |
84 by (cut_facts_tac prems 1); |
85 by (res_inst_tac [("Q","y===x")] (excluded_middle RS disjE) 1);ba 1; |
85 by (res_inst_tac [("Q","y===x")] (excluded_middle RS disjE) 1);by (assume_tac 1); |
86 bd sym2refl2 1; |
86 by (dtac sym2refl2 1); |
87 by (fast_tac set_cs 1); |
87 by (fast_tac set_cs 1); |
88 qed "notDomainE2"; |
88 qed "notDomainE2"; |
89 |
89 |
90 (* theorems for equivalence relations *) |
90 (* theorems for equivalence relations *) |
91 goal thy "(x::'a::er) : D"; |
91 goal thy "(x::'a::er) : D"; |
92 br DomainI 1; |
92 by (rtac DomainI 1); |
93 br er_refl 1; |
93 by (rtac er_refl 1); |
94 qed "er_Domain"; |
94 qed "er_Domain"; |
95 |
95 |
96 (* witnesses for "=>" ::(per,per)per *) |
96 (* witnesses for "=>" ::(per,per)per *) |
97 val prems = goalw thy [fun_per_def]"eqv (x::'a::per => 'b::per) y ==> eqv y x"; |
97 val prems = goalw thy [fun_per_def]"eqv (x::'a::per => 'b::per) y ==> eqv y x"; |
98 by (cut_facts_tac prems 1); |
98 by (cut_facts_tac prems 1); |
104 "[| eqv (f::'a::per=>'b::per) g;eqv g h|] ==> eqv f h"; |
104 "[| eqv (f::'a::per=>'b::per) g;eqv g h|] ==> eqv f h"; |
105 by (cut_facts_tac prems 1); |
105 by (cut_facts_tac prems 1); |
106 by (safe_tac HOL_cs); |
106 by (safe_tac HOL_cs); |
107 by (REPEAT (dtac spec 1)); |
107 by (REPEAT (dtac spec 1)); |
108 by (res_inst_tac [("y","g y")] per_trans 1); |
108 by (res_inst_tac [("y","g y")] per_trans 1); |
109 br mp 1;ba 1; |
109 by (rtac mp 1);by (assume_tac 1); |
110 by (Asm_simp_tac 1); |
110 by (Asm_simp_tac 1); |
111 br mp 1;ba 1; |
111 by (rtac mp 1);by (assume_tac 1); |
112 by (asm_simp_tac (!simpset addsimps [sym2refl2]) 1); |
112 by (asm_simp_tac (!simpset addsimps [sym2refl2]) 1); |
113 qed "per_trans_fun"; |
113 qed "per_trans_fun"; |
114 |
114 |
115 |
115 |