--- a/QuotMain.thy	Wed Oct 21 13:47:39 2009 +0200
+++ b/QuotMain.thy	Wed Oct 21 14:09:06 2009 +0200
@@ -471,10 +471,11 @@
   val thm' = forall_intr_vars thm
   val thm'' = ObjectLogic.atomize (cprop_of thm')
 in
-  Simplifier.rewrite_rule [thm''] thm'
+  Thm.freezeT (Simplifier.rewrite_rule [thm''] thm')
 end
 *}
 
+ML {* atomize_thm @{thm list.induct} *}
 
 section {* REGULARIZE *}
 
@@ -703,11 +704,18 @@
   trm == new_trm
 *)
 
-section {* TRANSCONV *}
+ML {*
+  fun build_regularize_goal thm rty rel lthy =
+     Logic.mk_implies
+       ((prop_of thm),
+       (regularise (prop_of thm) rty rel lthy))
+*}
+
+section {* RepAbs injection *}
 
 
 ML {*
-fun build_goal_term lthy thm constructors rty qty =
+fun build_repabs_term lthy thm constructors rty qty =
   let
     fun mk_rep tm =
       let
@@ -766,15 +774,16 @@
 *}
 
 ML {*
-fun build_goal ctxt thm cons rty qty =
-  Logic.mk_equals ((Thm.prop_of thm), (build_goal_term ctxt thm cons rty qty))
+fun build_repabs_goal ctxt thm cons rty qty =
+  Logic.mk_equals ((Thm.prop_of thm), (build_repabs_term ctxt thm cons rty qty))
 *}
 
 
 
 
 
-text {* finite set example *}
+section {* finite set example *}
+
 print_syntax
 inductive
   list_eq (infix "\<approx>" 50)
@@ -1058,7 +1067,7 @@
 
 ML {*
 cterm_of @{theory} (prop_of m1_novars);
-cterm_of @{theory} (build_goal_term @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"});
+cterm_of @{theory} (build_repabs_term @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"});
 *}
 
 
@@ -1081,7 +1090,7 @@
 
 ML {*
   val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm m1}))
-  val goal = build_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"}
+  val goal = build_repabs_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"}
   val cgoal = cterm_of @{theory} goal
   val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)
 *}
@@ -1097,7 +1106,7 @@
 thm length_append (* Not true but worth checking that the goal is correct *)
 ML {*
   val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm length_append}))
-  val goal = build_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"}
+  val goal = build_repabs_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"}
   val cgoal = cterm_of @{theory} goal
   val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)
 *}
@@ -1108,7 +1117,7 @@
 thm m2
 ML {*
   val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm m2}))
-  val goal = build_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"}
+  val goal = build_repabs_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"}
   val cgoal = cterm_of @{theory} goal
   val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)
 *}
@@ -1119,7 +1128,7 @@
 thm list_eq.intros(4)
 ML {*
   val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm list_eq.intros(4)}))
-  val goal = build_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"}
+  val goal = build_repabs_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"}
   val cgoal = cterm_of @{theory} goal
   val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false fset_defs_sym cgoal)
   val cgoal3 = Thm.rhs_of (MetaSimplifier.rewrite true @{thms QUOT_TYPE_I_fset.thm10} cgoal2)
@@ -1141,7 +1150,7 @@
 thm list_eq.intros(5)
 ML {*
   val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm list_eq.intros(5)}))
-  val goal = build_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"}
+  val goal = build_repabs_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"}
   val cgoal = cterm_of @{theory} goal
   val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal)
 *}
@@ -1160,12 +1169,10 @@
 ML {* atomize_thm @{thm list_induct_hol4} *}
 
 
-ML {* val li = Thm.freezeT (atomize_thm @{thm list_induct_hol4}) *}
+ML {* val li = atomize_thm @{thm list_induct_hol4} *}
 
 prove list_induct_r: {*
- Logic.mk_implies
-   ((prop_of li),
-   (regularise (prop_of li) @{typ "'a List.list"} @{term "op \<approx>"} @{context})) *}
+   build_regularize_goal (atomize_thm @{thm list_induct_hol4}) @{typ "'a List.list"} @{term "op \<approx>"} @{context} *}
   apply (simp only: equiv_res_forall[OF equiv_list_eq])
   thm RIGHT_RES_FORALL_REGULAR
   apply (rule RIGHT_RES_FORALL_REGULAR)
@@ -1175,12 +1182,12 @@
   done
 
 ML {* val thm = @{thm list_induct_r} OF [li] *}
-ML {* val trm_r = build_goal @{context} thm consts @{typ "'a list"} @{typ "'a fset"} *}
+ML {* val trm_r = build_repabs_goal @{context} thm consts @{typ "'a list"} @{typ "'a fset"} *}
 lemmas APPLY_RSP_I = APPLY_RSP[of "(op \<approx> ===> op =) ===> op =" "(ABS_fset ---> id) ---> id" "(REP_fset ---> id) ---> id" "op =" "id" "id"]
 lemmas REP_ABS_RSP_I = REP_ABS_RSP(1)[of "(op \<approx> ===> op =) ===> op =" "(ABS_fset ---> id) ---> id" "(REP_fset ---> id) ---> id"]
 lemmas APPLY_RSP_II = APPLY_RSP[of "op \<approx>" "ABS_fset" "REP_fset" "op \<approx>" "ABS_fset" "REP_fset"]
 
-ML {* val trm = build_goal_term @{context} thm consts @{typ "'a list"} @{typ "'a fset"} *}
+ML {* val trm = build_repabs_term @{context} thm consts @{typ "'a list"} @{typ "'a fset"} *}
 
 
 prove list_induct_tr: trm_r
@@ -1384,7 +1391,7 @@
   fun lift_theorem_fset_aux thm lthy =
     let
       val ((_, [novars]), lthy2) = Variable.import true [thm] lthy;
-      val goal = build_goal @{context} novars consts @{typ "'a list"} @{typ "'a fset"};
+      val goal = build_repabs_goal @{context} novars consts @{typ "'a list"} @{typ "'a fset"};
       val cgoal = cterm_of @{theory} goal;
       val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal);
       val tac = transconv_fset_tac' @{context};