--- a/QuotMain.thy Wed Oct 21 14:09:06 2009 +0200
+++ b/QuotMain.thy Wed Oct 21 14:15:22 2009 +0200
@@ -704,6 +704,7 @@
trm == new_trm
*)
+text {* Assumes that the given theorem is atomized *}
ML {*
fun build_regularize_goal thm rty rel lthy =
Logic.mk_implies
@@ -713,7 +714,6 @@
section {* RepAbs injection *}
-
ML {*
fun build_repabs_term lthy thm constructors rty qty =
let
@@ -773,18 +773,15 @@
end
*}
+text {* Assumes that it is given a regularized theorem *}
ML {*
fun build_repabs_goal ctxt thm cons rty qty =
Logic.mk_equals ((Thm.prop_of thm), (build_repabs_term ctxt thm cons rty qty))
*}
-
-
-
section {* finite set example *}
-print_syntax
inductive
list_eq (infix "\<approx>" 50)
where
@@ -1041,26 +1038,14 @@
done
ML {*
- fun mk_rep x = @{term REP_fset} $ x;
- fun mk_abs x = @{term ABS_fset} $ x;
val consts = [@{const_name "Nil"}, @{const_name "Cons"},
@{const_name "membship"}, @{const_name "card1"},
@{const_name "append"}, @{const_name "fold1"}];
*}
-ML {* val tm = @{term "x :: 'a list"} *}
-ML {* val ty = exchange_ty @{typ "'a list"} @{typ "'a fset"} (fastype_of tm) *}
-ML {* (fst (get_fun repF @{typ "'a list"} @{typ "'a fset"} @{context} ty)) $ tm *}
-
-ML {* val qty = @{typ "'a fset"} *}
-ML {* val tt = Type ("fun", [Type ("fun", [qty, @{typ "prop"}]), @{typ "prop"}]) *}
-ML {* val fall = Const(@{const_name all}, dummyT) *}
-
ML {* val fset_defs = @{thms EMPTY_def IN_def UNION_def card_def INSERT_def} *}
ML {* val fset_defs_sym = map (fn t => symmetric (unabs_def @{context} t)) fset_defs *}
-
-
ML {*
val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm m2}))
*}