equal
deleted
inserted
replaced
20 bn::"assg \<Rightarrow> atom set" |
20 bn::"assg \<Rightarrow> atom set" |
21 where |
21 where |
22 "bn (As x y t) = {atom x}" |
22 "bn (As x y t) = {atom x}" |
23 |
23 |
24 (* can lift *) |
24 (* can lift *) |
|
25 |
25 thm distinct |
26 thm distinct |
26 thm trm_raw_assg_raw.inducts |
27 thm trm_raw_assg_raw.inducts |
27 thm fv_defs |
28 thm fv_defs |
28 thm perm_simps |
29 thm perm_simps |
29 thm perm_laws |
30 thm perm_laws |
55 |
56 |
56 ML {* |
57 ML {* |
57 val thms_f = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms perm_laws} |
58 val thms_f = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms perm_laws} |
58 *} |
59 *} |
59 |
60 |
60 |
61 ML {* |
|
62 Local_Theory.exit_global; |
|
63 Class.instantiation; |
|
64 Class.prove_instantiation_exit_result; |
|
65 Named_Target.theory_init; |
|
66 op |-> |
|
67 *} |
|
68 |
|
69 done |
|
70 |> ... |
|
71 |-> (fn x => Class.prove_instantiation_exit_result phi tac x) |
|
72 |-> (fn y => ...) |
61 |
73 |
62 |
74 |
63 |
75 |
64 section {* NOT *} |
76 section {* NOT *} |
65 |
77 |
85 |
97 |
86 ML {* |
98 ML {* |
87 val thms_e = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms eq_iff[unfolding alphas]} |
99 val thms_e = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms eq_iff[unfolding alphas]} |
88 *} |
100 *} |
89 |
101 |
90 section {* NOT *} |
|
91 |
|
92 ML {* |
|
93 val thms_p = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms perm_simps(1)} |
|
94 *} |
|
95 |
|
96 instance trm :: pt sorry |
|
97 instance assg :: pt sorry |
|
98 |
|
99 |
|
100 |
|
101 |
|
102 |
|
103 |
|
104 |
|
105 |
|
106 |
|
107 |
|
108 thm eq_iff[no_vars] |
|
109 |
|
110 ML {* |
|
111 val q1 = lift_thm [@{typ trm}, @{typ assg}] @{context} @{thm "eq_iff"(1)} |
|
112 *} |
|
113 |
|
114 local_setup {* Local_Theory.note ((@{binding d1}, []), thms_d) #> snd *} |
|
115 local_setup {* Local_Theory.note ((@{binding i1}, []), thms_i) #> snd *} |
|
116 local_setup {* Local_Theory.note ((@{binding f1}, []), thms_f) #> snd *} |
|
117 local_setup {* Local_Theory.note ((@{binding q1}, []), [q1]) #> snd *} |
|
118 |
|
119 |
102 |
120 thm perm_defs |
103 thm perm_defs |
121 thm perm_simps |
104 thm perm_simps |
122 |
105 |
123 lemma supp_fv: |
106 lemma supp_fv: |
134 |
117 |
135 lemma y: |
118 lemma y: |
136 "perm_bn_trm p (Var x) = (Var x)" |
119 "perm_bn_trm p (Var x) = (Var x)" |
137 "perm_bn_trm p (App t1 t2) = (App t1 t2)" |
120 "perm_bn_trm p (App t1 t2) = (App t1 t2)" |
138 "perm_bn_trm p (" |
121 "perm_bn_trm p (" |
139 |
|
140 |
|
141 |
|
142 ML {* |
|
143 map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms eq_iff} |
|
144 *} |
|
145 |
|
146 |
|
147 |
|
148 |
|
149 |
|
150 lemma "Var x \<noteq> App y1 y2" |
|
151 apply(descending) |
|
152 apply(simp add: trm_raw.distinct) |
|
153 |
|
154 |
|
155 |
|
156 ML {* |
|
157 map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms trm_raw.distinct(1)} |
|
158 *} |
|
159 |
|
160 |
122 |
161 |
123 |
162 |
124 |
163 typ trm |
125 typ trm |
164 typ assg |
126 typ assg |