
diff -r e6b6e5ba0cc5 -r 553bef083318 FSet.thy
--- a/FSet.thy	Mon Nov 23 13:55:31 2009 +0100
+++ b/FSet.thy	Mon Nov 23 14:05:02 2009 +0100
@@ -439,178 +439,8 @@
 ML {* val glf = Type.legacy_freeze gla *}
 ML {* val glac = (snd o Thm.dest_equals o cprop_of) (ObjectLogic.atomize (cterm_of @{theory} glf)) *}
 
-ML {*
-fun apply_subt2 f trm trm2 =
-  case (trm, trm2) of
-    (Abs (x, T, t), Abs (x2, T2, t2)) =>
-       let
-         val (x', t') = Term.dest_abs (x, T, t);
-         val (x2', t2') = Term.dest_abs (x2, T2, t2)
-         val (s1, s2) = f t' t2';
-       in
-         (Term.absfree (x', T, s1),
-          Term.absfree (x2', T2, s2))
-       end
-  | _ => f trm trm2
-*}
-
-(*ML_prf {*
-val concl = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ()))))
-val pat = Drule.strip_imp_concl (cprop_of @{thm APPLY_RSP2})
-val insts = Thm.first_order_match (pat, concl)
-val t = Drule.instantiate insts @{thm APPLY_RSP2}
-*}*)
-
-ML {*
-fun tyRel2 lthy ty gty =
-  if ty = gty then HOLogic.eq_const ty else
-
-  case quotdata_lookup lthy (fst (dest_Type gty)) of
-    SOME quotdata =>
-      if Sign.typ_instance (ProofContext.theory_of lthy) (ty, #rtyp quotdata) then
-        case #rel quotdata of
-          Const(s, _) => Const(s, dummyT)
-        | _ => error "tyRel2 fail: relation is not a constant"
-      else error "tyRel2 fail: a non-lifted type lifted to a lifted type"
-  | NONE => (case (ty, gty) of
-      (Type (s, tys), Type (s2, tys2)) =>
-      if s = s2 andalso length tys = length tys2 then
-        let
-          val tys_rel = map (fn ty => ty --> ty --> @{typ bool}) tys;
-          val ty_out = ty --> ty --> @{typ bool};
-          val tys_out = tys_rel ---> ty_out;
-        in
-        (case (maps_lookup (ProofContext.theory_of lthy) s) of
-          SOME (info) => list_comb (Const (#relfun info, tys_out),
-                              map2 (tyRel2 lthy) tys tys2)
-        | NONE  => HOLogic.eq_const ty
-        )
-        end
-      else error "tyRel2 fail: different type structures"
-    | _ => HOLogic.eq_const ty)
-*}
-
-ML mk_babs
-
-ML {*
-fun mk_babs ty ty' = Const (@{const_name "Babs"}, [ty' --> @{typ bool}, ty] ---> ty)
-fun mk_ball ty = Const (@{const_name "Ball"}, [ty, ty] ---> @{typ bool})
-fun mk_bex ty = Const (@{const_name "Bex"}, [ty, ty] ---> @{typ bool})
-fun mk_resp ty = Const (@{const_name Respects}, [[ty, ty] ---> @{typ bool}, ty] ---> @{typ bool})
-*}
-
+prove t_r: {* mk_REGULARIZE_goal @{context} (prop_of t_a) (term_of glac) *}
 
-ML {*
-fun my_reg2 lthy trm gtrm =
-  case (trm, gtrm) of
-    (Abs (x, T, t), Abs (x2, T2, t2)) =>
-       if not (T = T2) then
-         let
-           val rrel = tyRel2 lthy T T2;
-           val (s1, s2) = apply_subt2 (my_reg2 lthy) trm gtrm
-         in
-           (((mk_babs (fastype_of trm) T) $ (mk_resp T $ rrel) $ s1),
-           ((mk_babs (fastype_of gtrm) T2) $ (mk_resp T2 $ (HOLogic.eq_const dummyT)) $ s2))
-         end
-       else
-         let
-           val (s1, s2) = apply_subt2 (my_reg2 lthy) t t2
-         in
-           (Abs(x, T, s1), Abs(x2, T2, s2))
-         end
-  | (Const (@{const_name "All"}, ty) $ (t as Abs (_, T, _)),
-     Const (@{const_name "All"}, ty') $ (t2 as Abs (_, T2, _))) =>
-       if not (T = T2) then
-         let
-            val ty1 = domain_type ty;
-            val ty2 = domain_type ty1;
-            val ty'1 = domain_type ty';
-            val ty'2 = domain_type ty'1;
-            val rrel = tyRel2 lthy T T2;
-            val (s1, s2) = apply_subt2 (my_reg2 lthy) t t2;
-         in
-           (((mk_ball ty1) $ (mk_resp ty2 $ rrel) $ s1),
-           ((mk_ball ty'1) $ (mk_resp ty'2 $ (HOLogic.eq_const dummyT)) $ s2))
-         end
-       else
-         let
-           val (s1, s2) = apply_subt2 (my_reg2 lthy) t t2
-         in
-           ((Const (@{const_name "All"}, ty) $ s1),
-           (Const (@{const_name "All"}, ty') $ s2))
-         end
-  | (Const (@{const_name "Ex"}, ty) $ (t as Abs (_, T, _)),
-     Const (@{const_name "Ex"}, ty') $ (t2 as Abs (_, T2, _))) =>
-       if not (T = T2) then
-         let
-            val ty1 = domain_type ty
-            val ty2 = domain_type ty1
-            val ty'1 = domain_type ty'
-            val ty'2 = domain_type ty'1
-            val rrel = tyRel2 lthy T T2
-            val (s1, s2) = apply_subt2 (my_reg2 lthy) t t2
-         in
-           (((mk_bex ty1) $ (mk_resp ty2 $ rrel) $ s1),
-           ((mk_bex ty'1) $ (mk_resp ty'2 $ (HOLogic.eq_const dummyT)) $ s2))
-         end
-       else
-         let
-           val (s1, s2) = apply_subt2 (my_reg2 lthy) t t2
-         in
-           ((Const (@{const_name "Ex"}, ty) $ s1),
-           (Const (@{const_name "Ex"}, ty') $ s2))
-         end
-  | (Const (@{const_name "op ="}, T) $ t, (Const (@{const_name "op ="}, T2) $ t2)) =>
-      let
-        val (s1, s2) = apply_subt2 (my_reg2 lthy) t t2
-        val rhs = Const (@{const_name "op ="}, T2) $ s2
-      in
-        if not (T = T2) then
-          ((tyRel2 lthy T T2) $ s1, rhs)
-        else
-          (Const (@{const_name "op ="}, T) $ s1, rhs)
-      end
-  | (t $ t', t2 $ t2') =>
-      let
-        val (s1, s2) = apply_subt2 (my_reg2 lthy) t t2
-        val (s1', s2') = apply_subt2 (my_reg2 lthy) t' t2'
-      in
-        (s1 $ s1', s2 $ s2')
-      end
-  | (Const c1, Const c2) => (Const c1, Const c2) (* c2 may be lifted *)
-  | (Bound i, Bound j) => (* Bounds are replaced, so should never happen? *)
-      if i = j then (Bound i, Bound j) else error "my_reg2: different Bounds"
-  | (Free (n, T), Free(n2, T2)) => if n = n2 then (Free (n, T), Free (n2, T2))
-      else error ("my_ref2: different variables: " ^ n ^ ", " ^ n2)
-  | _ => error "my_reg2: terms don't agree"
-*}
-
-
-ML {* prop_of t_a *}
-ML {* term_of glac *}
-ML {* val (tta, ttb) = (my_reg2 @{context} (prop_of t_a) (term_of glac)) *}
-
-(* Does not work. *)
-ML {* 
-  prop_of t_a 
-  |> Syntax.string_of_term @{context}
-  |> writeln
-*}
-
-ML {* 
-  (term_of glac) 
-  |> Syntax.string_of_term @{context}
-  |> writeln
-*}
-
-ML {* val tta = REGULARIZE_trm @{context} (prop_of t_a) (term_of glac) *} 
-
-ML {* val tt = Syntax.check_term @{context} tta *}
-
-
-
-prove t_r: {* Logic.mk_implies
-       ((prop_of t_a), tt) *}
 ML_prf {*  fun tac ctxt = FIRST' [
       rtac rel_refl,
       atac,
@@ -631,66 +461,9 @@
 
 ML {* val t_r = @{thm t_r} OF [t_a] *}
 
-ML {* val ttg = Syntax.check_term @{context} ttb *}
-
-ML {*
-fun is_lifted_const h gh = is_Const h andalso is_Const gh andalso not (h = gh)
-
-fun mkrepabs lthy ty gty t =
-  let
-    val qenv = distinct (op=) (diff (gty, ty) [])
-(*  val _ = sanity_chk qenv lthy *)
-    val ty = fastype_of t
-    val abs = get_fun absF qenv lthy gty $ t
-    val rep = get_fun repF qenv lthy gty $ abs
-  in
-    Syntax.check_term lthy rep
-  end
-*}
-
-ML {*
-  cterm_of @{theory} (mkrepabs @{context} @{typ "'a list \<Rightarrow> bool"} @{typ "'a fset \<Rightarrow> bool"} @{term "f :: ('a list \<Rightarrow> bool)"})
-*}
-
-
-
-ML {*
-fun build_repabs_term lthy trm gtrm =
-  case (trm, gtrm) of
-    (Abs (a as (_, T, _)), Abs (a2 as (_, T2, _))) =>
-      let
-        val (vs, t) = Term.dest_abs a;
-        val (_,  g) = Term.dest_abs a2;
-        val v = Free(vs, T);
-        val t' = lambda v (build_repabs_term lthy t g);
-        val ty = fastype_of trm;
-        val gty = fastype_of gtrm;
-      in
-        if (ty = gty) then t' else
-        mkrepabs lthy ty gty (
-          if (T = T2) then t' else
-          lambda v (t' $ (mkrepabs lthy T T2 v))
-        )
-      end
-  | _ =>
-    case (Term.strip_comb trm, Term.strip_comb gtrm) of
-      ((Const(@{const_name Respects}, _), _), _) => trm
-    | ((h, tms), (gh, gtms)) =>
-      let
-        val ty = fastype_of trm;
-        val gty = fastype_of gtrm;
-        val tms' = map2 (build_repabs_term lthy) tms gtms
-        val t' = list_comb(h, tms')
-      in
-        if ty = gty then t' else
-        if is_lifted_const h gh then mkrepabs lthy ty gty t' else
-        if (Term.is_Free h) andalso (length tms > 0) then mkrepabs lthy ty gty t' else t'
-      end
-*}
-
-ML {* val ttt = build_repabs_term @{context} tt ttg *}
+ML {* val ttt = mk_inj_REPABS_goal @{context} (prop_of t_r, term_of glac) *}
 ML {* val si = simp_ids_trm (cterm_of @{theory} ttt) *}
-prove t_t: {* Logic.mk_equals ((Thm.prop_of t_r), term_of si) *}
+prove t_t: {* term_of si *}
 ML_prf {* fun r_mk_comb_tac_fset lthy = r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms *}
 apply(atomize(full))
 apply (tactic {* (APPLY_RSP_TAC rty @{context}) 1 *})




