1 open Witness; |
|
2 |
|
3 (* -------------------------------------------------------------------- *) |
|
4 (* classes cplus, cminus, ctimes, cdiv introduce |
|
5 characteristic constants o+ o- o* o/ |
|
6 |
|
7 "circ":: "one -> one -> one" |
|
8 |
|
9 is the witness for o+ o- o* o/ |
|
10 |
|
11 No characteristic axioms are to be checked |
|
12 *) |
|
13 |
|
14 (* -------------------------------------------------------------------- *) |
|
15 (* classes per and qpo introduce characteristic constants |
|
16 ".=" :: "'a::per -> 'a -> tr" (cinfixl 55) |
|
17 ".<=" :: "'a::qpo -> 'a -> tr" (cinfixl 55) |
|
18 |
|
19 The witness for these is |
|
20 |
|
21 "bullet":: "one -> one -> tr" (cinfixl 55) |
|
22 |
|
23 the classes equiv, eq, impose additional axioms |
|
24 *) |
|
25 |
|
26 (* -------------------------------------------------------------------- *) |
|
27 (* |
|
28 |
|
29 characteristic axioms of class per: |
|
30 |
|
31 strict_per "(UU .= x) = UU & (x .= UU) = UU" |
|
32 total_per "[|x ~= UU; y ~= UU|] ==> (x .= y) ~= UU" |
|
33 flat_per "flat (UU::'a::per)" |
|
34 |
|
35 sym_per "(x .= y) = (y .= x)" |
|
36 trans_per "[|(x .= y)=TT; (y .= z)=TT |] ==> (x .= z)=TT" |
|
37 |
|
38 -------------------------------------------------------------------- |
|
39 |
|
40 characteristic axioms of class equiv: |
|
41 |
|
42 refl_per "[|(x::'a::equiv) ~= UU|] ==> (x .= x)=TT" |
|
43 |
|
44 -------------------------------------------------------------------- |
|
45 |
|
46 characteristic axioms of class eq: |
|
47 |
|
48 weq "[|(x::'a::eq)~=UU; y~=UU|] ==> (x=y --> (x.=y)=TT) & (x~=y --> Çx.=yÈ)" |
|
49 |
|
50 |
|
51 -------------------------------------------------------------------- |
|
52 |
|
53 *) |
|
54 |
|
55 (* strict_per, strict_qpo *) |
|
56 goalw thy [bullet_def] "(UU bullet x) = UU & (x bullet UU) = UU"; |
|
57 by (simp_tac (!simpset addsimps [flift1_def,flift2_def,o_def]) 1); |
|
58 by (lift.induct_tac "x" 1); |
|
59 auto(); |
|
60 result(); |
|
61 |
|
62 (* total_per, total_qpo *) |
|
63 val prems = goal thy "[|x~=UU; y~=UU|] ==> (x bullet y) ~= UU"; |
|
64 by (subgoal_tac "x~=UU&y~=UU-->(x bullet y) ~= UU" 1); |
|
65 by (cut_facts_tac prems 1); |
|
66 by (fast_tac HOL_cs 1); |
|
67 by (simp_tac (!simpset addsimps [bullet_def,flift1_def,flift2_def,o_def]) 1); |
|
68 by (lift.induct_tac "x" 1); |
|
69 by (fast_tac HOL_cs 1); |
|
70 by (lift.induct_tac "y" 1); |
|
71 auto(); |
|
72 result(); |
|
73 |
|
74 (* flat_per *) |
|
75 |
|
76 goal thy "flat (x::one)"; |
|
77 by (rtac flat_flat 1); |
|
78 result(); |
|
79 |
|
80 (* sym_per *) |
|
81 goalw thy [bullet_def] "(x bullet y) = (y bullet x)"; |
|
82 by (simp_tac (!simpset addsimps [bullet_def,flift1_def,flift2_def,o_def]) 1); |
|
83 by (lift.induct_tac "x" 1); |
|
84 by (lift.induct_tac "y" 2); |
|
85 by (lift.induct_tac "y" 1); |
|
86 auto(); |
|
87 result(); |
|
88 |
|
89 (* trans_per, trans_qpo *) |
|
90 val prems = goal thy "[|(x bullet y)=TT; (y bullet z)=TT|] ==>(x bullet z)=TT"; |
|
91 by (subgoal_tac "(x bullet y)=TT&(y bullet z)=TT-->(x bullet z)=TT" 1); |
|
92 by (cut_facts_tac prems 1); |
|
93 by (fast_tac HOL_cs 1); |
|
94 by (simp_tac (!simpset addsimps [bullet_def,flift1_def,flift2_def,o_def]) 1); |
|
95 by (lift.induct_tac "x" 1); |
|
96 by (lift.induct_tac "y" 2); |
|
97 by (lift.induct_tac "y" 1); |
|
98 by (lift.induct_tac "z" 4); |
|
99 by (lift.induct_tac "z" 3); |
|
100 by (lift.induct_tac "z" 2); |
|
101 by (lift.induct_tac "z" 1); |
|
102 auto(); |
|
103 result(); |
|
104 |
|
105 (* refl_per *) |
|
106 val prems = goal thy "x ~= UU ==> (x bullet x)=TT"; |
|
107 by (subgoal_tac "x ~= UU --> (x bullet x)=TT" 1); |
|
108 by (cut_facts_tac prems 1); |
|
109 by (fast_tac HOL_cs 1); |
|
110 by (simp_tac (!simpset addsimps [bullet_def,flift1_def,flift2_def,o_def]) 1); |
|
111 by (lift.induct_tac "x" 1); |
|
112 auto(); |
|
113 qed "refl_per_one"; |
|