equal
deleted
inserted
replaced
79 Toplevel.context_of; |
79 Toplevel.context_of; |
80 Toplevel.keep |
80 Toplevel.keep |
81 *} |
81 *} |
82 |
82 |
83 ML {* |
83 ML {* |
84 get_fun repF @{typ t} @{typ qt} @{context} @{typ "((((qt \<Rightarrow> qt) \<Rightarrow> qt) \<Rightarrow> qt) list) * nat"} |
84 get_fun repF [(@{typ qt}, @{typ qt})] @{context} @{typ "((((qt \<Rightarrow> qt) \<Rightarrow> qt) \<Rightarrow> qt) list) * nat"} |
85 |> fst |
85 |> fst |
86 |> Syntax.string_of_term @{context} |
86 |> Syntax.string_of_term @{context} |
87 |> writeln |
87 |> writeln |
88 *} |
88 *} |
89 |
89 |
90 ML {* |
90 ML {* |
91 get_fun absF @{typ t} @{typ qt} @{context} @{typ "qt * nat"} |
91 get_fun absF [(@{typ qt}, @{typ t})] @{context} @{typ "qt * nat"} |
92 |> fst |
92 |> fst |
93 |> Syntax.string_of_term @{context} |
93 |> Syntax.string_of_term @{context} |
94 |> writeln |
94 |> writeln |
95 *} |
95 *} |
96 |
96 |
97 ML {* |
97 ML {* |
98 get_fun absF @{typ t} @{typ qt} @{context} @{typ "(qt \<Rightarrow> qt) \<Rightarrow> qt"} |
98 get_fun absF [(@{typ qt}, @{typ t})] @{context} @{typ "(qt \<Rightarrow> qt) \<Rightarrow> qt"} |
99 |> fst |
99 |> fst |
100 |> Syntax.pretty_term @{context} |
100 |> Syntax.pretty_term @{context} |
101 |> Pretty.string_of |
101 |> Pretty.string_of |
102 |> writeln |
102 |> writeln |
103 *} |
103 *} |
109 make_const_def @{binding bla'} @{term "bla"} NoSyn @{typ "t"} @{typ "qt"} lthy |
109 make_const_def @{binding bla'} @{term "bla"} NoSyn @{typ "t"} @{typ "qt"} lthy |
110 )) |> snd |
110 )) |> snd |
111 *} |
111 *} |
112 *) |
112 *) |
113 |
113 |
114 local_setup {* |
114 quotient_def (for qt) |
115 make_const_def @{binding VR} @{term "vr"} NoSyn @{typ "t"} @{typ "qt"} #> snd #> |
115 VR ::"string \<Rightarrow> qt" |
116 make_const_def @{binding AP} @{term "ap"} NoSyn @{typ "t"} @{typ "qt"} #> snd #> |
116 where |
117 make_const_def @{binding LM} @{term "lm"} NoSyn @{typ "t"} @{typ "qt"} #> snd |
117 "VR \<equiv> vr" |
118 *} |
118 |
|
119 quotient_def (for qt) |
|
120 AP ::"qt list \<Rightarrow> qt" |
|
121 where |
|
122 "AP \<equiv> ap" |
|
123 |
|
124 quotient_def (for qt) |
|
125 LM ::"string \<Rightarrow> qt \<Rightarrow> qt" |
|
126 where |
|
127 "LM \<equiv> lm" |
119 |
128 |
120 term vr |
129 term vr |
121 term ap |
130 term ap |
122 term lm |
131 term lm |
123 thm VR_def AP_def LM_def |
132 thm VR_def AP_def LM_def |
139 done |
148 done |
140 |
149 |
141 print_quotients |
150 print_quotients |
142 print_theorems |
151 print_theorems |
143 |
152 |
144 local_setup {* |
153 |
145 make_const_def @{binding VR'} @{term "vr'"} NoSyn @{typ "'a t'"} @{typ "'a qt'"} #> snd #> |
154 quotient_def (for "'a qt'") |
146 make_const_def @{binding AP'} @{term "ap'"} NoSyn @{typ "'a t'"} @{typ "'a qt'"} #> snd #> |
155 VR' ::"string \<Rightarrow> 'a qt" |
147 make_const_def @{binding LM'} @{term "lm'"} NoSyn @{typ "'a t'"} @{typ "'a qt'"} #> snd |
156 where |
148 *} |
157 "VR' \<equiv> vr'" |
|
158 |
|
159 quotient_def (for "'a qt'") |
|
160 AP' ::"('a qt') * ('a qt') \<Rightarrow> 'a qt" |
|
161 where |
|
162 "AP' \<equiv> ap'" |
|
163 |
|
164 quotient_def (for "'a qt'") |
|
165 LM' ::"'a \<Rightarrow> string \<Rightarrow> 'a qt'" |
|
166 where |
|
167 "LM' \<equiv> lm'" |
149 |
168 |
150 term vr' |
169 term vr' |
151 term ap' |
170 term ap' |
152 term ap' |
171 term ap' |
153 thm VR'_def AP'_def LM'_def |
172 thm VR'_def AP'_def LM'_def |