# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1256125659 -7200
# Node ID 4cc5db28b1c3bf1dbeffb3e8cfc5b80989ffa532
# Parent  59bba5cfa24879408a30d1893adab274b7a04ec0
Reordering

diff -r 59bba5cfa248 -r 4cc5db28b1c3 QuotMain.thy
--- a/QuotMain.thy	Wed Oct 21 11:50:53 2009 +0200
+++ b/QuotMain.thy	Wed Oct 21 13:47:39 2009 +0200
@@ -411,6 +411,368 @@
 term VR'
 term AP'
 
+section {* ATOMIZE *}
+
+text {*
+  Unabs_def converts a definition given as
+
+    c \<equiv> %x. %y. f x y
+
+  to a theorem of the form
+
+    c x y \<equiv> f x y
+
+  This function is needed to rewrite the right-hand
+  side to the left-hand side.
+*}
+
+ML {*
+fun unabs_def ctxt def =
+let
+  val (lhs, rhs) = Thm.dest_equals (cprop_of def)
+  val xs = strip_abs_vars (term_of rhs)
+  val (_, ctxt') = Variable.add_fixes (map fst xs) ctxt
+
+  val thy = ProofContext.theory_of ctxt'
+  val cxs = map (cterm_of thy o Free) xs
+  val new_lhs = Drule.list_comb (lhs, cxs)
+
+  fun get_conv [] = Conv.rewr_conv def
+    | get_conv (x::xs) = Conv.fun_conv (get_conv xs)
+in
+  get_conv xs new_lhs |>
+  singleton (ProofContext.export ctxt' ctxt)
+end
+*}
+
+lemma atomize_eqv[atomize]: 
+  shows "(Trueprop A \<equiv> Trueprop B) \<equiv> (A \<equiv> B)" 
+proof
+  assume "A \<equiv> B" 
+  then show "Trueprop A \<equiv> Trueprop B" by unfold
+next
+  assume *: "Trueprop A \<equiv> Trueprop B"
+  have "A = B"
+  proof (cases A)
+    case True
+    have "A" by fact
+    then show "A = B" using * by simp
+  next
+    case False
+    have "\<not>A" by fact
+    then show "A = B" using * by auto
+  qed
+  then show "A \<equiv> B" by (rule eq_reflection)
+qed
+
+ML {*
+fun atomize_thm thm =
+let
+  val thm' = forall_intr_vars thm
+  val thm'' = ObjectLogic.atomize (cprop_of thm')
+in
+  Simplifier.rewrite_rule [thm''] thm'
+end
+*}
+
+
+section {* REGULARIZE *}
+
+text {* tyRel takes a type and builds a relation that a quantifier over this
+  type needs to respect. *}
+ML {*
+fun tyRel ty rty rel lthy =
+  if ty = rty 
+  then rel
+  else (case ty of
+          Type (s, tys) =>
+            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), map (fn ty => tyRel ty rty rel lthy) tys)
+             | NONE  => HOLogic.eq_const ty
+            )
+            end
+        | _ => HOLogic.eq_const ty)
+*}
+
+ML {*
+  cterm_of @{theory} (tyRel @{typ "trm \<Rightarrow> bool"} @{typ "trm"} @{term "RR"} @{context})
+*}
+
+definition
+  Babs :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
+where
+  "(x \<in> p) \<Longrightarrow> (Babs p m x = m x)"
+(* TODO: Consider defining it with an "if"; sth like:
+   Babs p m = \<lambda>x. if x \<in> p then m x else undefined
+*)
+
+ML {*
+fun needs_lift (rty as Type (rty_s, _)) ty =
+  case ty of
+    Type (s, tys) =>
+      (s = rty_s) orelse (exists (needs_lift rty) tys)
+  | _ => false
+
+*}
+
+ML {*
+(* trm \<Rightarrow> new_trm *)
+fun regularise trm rty rel lthy =
+  case trm of
+    Abs (x, T, t) =>
+      if (needs_lift rty T) then let
+        val ([x'], lthy2) = Variable.variant_fixes [x] lthy;
+        val v = Free (x', T);
+        val t' = subst_bound (v, t);
+        val rec_term = regularise t' rty rel lthy2;
+        val lam_term = Term.lambda_name (x, v) rec_term;
+        val sub_res_term = tyRel T rty rel lthy;
+        val respects = Const (@{const_name Respects}, (fastype_of sub_res_term) --> T --> @{typ bool});
+        val res_term = respects $ sub_res_term;
+        val ty = fastype_of trm;
+        val rabs = Const (@{const_name Babs}, (fastype_of res_term) --> ty --> ty);
+        val rabs_term = (rabs $ res_term) $ lam_term;
+      in
+        rabs_term
+      end else let
+        val ([x'], lthy2) = Variable.variant_fixes [x] lthy;
+        val v = Free (x', T);
+        val t' = subst_bound (v, t);
+        val rec_term = regularise t' rty rel lthy2;
+      in
+        Term.lambda_name (x, v) rec_term
+      end
+  | ((Const (@{const_name "All"}, at)) $ (Abs (x, T, t))) =>
+      if (needs_lift rty T) then let
+        val ([x'], lthy2) = Variable.variant_fixes [x] lthy;
+        val v = Free (x', T);
+        val t' = subst_bound (v, t);
+        val rec_term = regularise t' rty rel lthy2;
+        val lam_term = Term.lambda_name (x, v) rec_term;
+        val sub_res_term = tyRel T rty rel lthy;
+        val respects = Const (@{const_name Respects}, (fastype_of sub_res_term) --> T --> @{typ bool});
+        val res_term = respects $ sub_res_term;
+        val ty = fastype_of lam_term;
+        val rall = Const (@{const_name Ball}, (fastype_of res_term) --> ty --> @{typ bool});
+        val rall_term = (rall $ res_term) $ lam_term;
+      in
+        rall_term
+      end else let
+        val ([x'], lthy2) = Variable.variant_fixes [x] lthy;
+        val v = Free (x', T);
+        val t' = subst_bound (v, t);
+        val rec_term = regularise t' rty rel lthy2;
+        val lam_term = Term.lambda_name (x, v) rec_term
+      in
+        Const(@{const_name "All"}, at) $ lam_term
+      end
+  | ((Const (@{const_name "All"}, at)) $ P) =>
+      let
+        val (_, [al, _]) = dest_Type (fastype_of P);
+        val ([x], lthy2) = Variable.variant_fixes [""] lthy;
+        val v = (Free (x, al));
+        val abs = Term.lambda_name (x, v) (P $ v);
+      in regularise ((Const (@{const_name "All"}, at)) $ abs) rty rel lthy2 end
+  | ((Const (@{const_name "Ex"}, at)) $ (Abs (x, T, t))) =>
+      if (needs_lift rty T) then let
+        val ([x'], lthy2) = Variable.variant_fixes [x] lthy;
+        val v = Free (x', T);
+        val t' = subst_bound (v, t);
+        val rec_term = regularise t' rty rel lthy2;
+        val lam_term = Term.lambda_name (x, v) rec_term;
+        val sub_res_term = tyRel T rty rel lthy;
+        val respects = Const (@{const_name Respects}, (fastype_of sub_res_term) --> T --> @{typ bool});
+        val res_term = respects $ sub_res_term;
+        val ty = fastype_of lam_term;
+        val rall = Const (@{const_name Bex}, (fastype_of res_term) --> ty --> @{typ bool});
+        val rall_term = (rall $ res_term) $ lam_term;
+      in
+        rall_term
+      end else let
+        val ([x'], lthy2) = Variable.variant_fixes [x] lthy;
+        val v = Free (x', T);
+        val t' = subst_bound (v, t);
+        val rec_term = regularise t' rty rel lthy2;
+        val lam_term = Term.lambda_name (x, v) rec_term
+      in
+        Const(@{const_name "Ex"}, at) $ lam_term
+      end
+  | ((Const (@{const_name "Ex"}, at)) $ P) =>
+      let
+        val (_, [al, _]) = dest_Type (fastype_of P);
+        val ([x], lthy2) = Variable.variant_fixes [""] lthy;
+        val v = (Free (x, al));
+        val abs = Term.lambda_name (x, v) (P $ v);
+      in regularise ((Const (@{const_name "Ex"}, at)) $ abs) rty rel lthy2 end
+  | a $ b => (regularise a rty rel lthy) $ (regularise b rty rel lthy)
+  | _ => trm
+
+*}
+
+ML {*
+  cterm_of @{theory} (regularise @{term "\<lambda>x :: int. x"} @{typ "trm"} @{term "RR"} @{context});
+  cterm_of @{theory} (regularise @{term "\<lambda>x :: trm. x"} @{typ "trm"} @{term "RR"} @{context});
+  cterm_of @{theory} (regularise @{term "\<forall>x :: trm. P x"} @{typ "trm"} @{term "RR"} @{context});
+  cterm_of @{theory} (regularise @{term "\<exists>x :: trm. P x"} @{typ "trm"} @{term "RR"} @{context});
+  cterm_of @{theory} (regularise @{term "All (P :: trm \<Rightarrow> bool)"} @{typ "trm"} @{term "RR"} @{context});
+*}
+
+(* my version of regularise *)
+(****************************)
+
+(* some helper functions *)
+
+
+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})
+*}
+
+(* applies f to the subterm of an abstractions, otherwise to the given term *)
+ML {*
+fun apply_subt f trm =
+  case trm of
+    Abs (x, T, t) => Abs (x, T, f t)
+  | _ => f trm
+*}
+
+
+(* FIXME: assumes always the typ is qty! *)
+(* FIXME: if there are more than one quotient, then you have to look up the relation *)
+ML {*
+fun my_reg rel trm =
+  case trm of
+    Abs (x, T, t) =>
+       let 
+          val ty1 = fastype_of trm
+       in
+         (mk_babs ty1 T) $ (mk_resp T $ rel) $ (Abs (x, T, my_reg rel t))    
+       end
+  | Const (@{const_name "All"}, ty) $ t =>
+       let 
+          val ty1 = domain_type ty
+          val ty2 = domain_type ty1
+       in
+         (mk_ball ty1) $ (mk_resp ty2 $ rel) $ (apply_subt (my_reg rel) t)      
+       end
+  | Const (@{const_name "Ex"}, ty) $ t =>
+       let 
+          val ty1 = domain_type ty
+          val ty2 = domain_type ty1
+       in
+         (mk_bex ty1) $ (mk_resp ty2 $ rel) $ (apply_subt (my_reg rel) t)    
+       end
+  | t1 $ t2 => (my_reg rel t1) $ (my_reg rel t2)
+  | _ => trm
+*}
+
+ML {*  
+  cterm_of @{theory} (regularise @{term "\<lambda>x::trm. x"} @{typ "trm"} @{term "RR"} @{context});
+  cterm_of @{theory} (my_reg @{term "RR"} @{term "\<lambda>x::trm. x"})
+*}
+
+ML {*  
+  cterm_of @{theory} (regularise @{term "\<forall>(x::trm) (y::trm). P x y"} @{typ "trm"} @{term "RR"} @{context});
+  cterm_of @{theory} (my_reg @{term "RR"} @{term "\<forall>(x::trm) (y::trm). P x y"})
+*}
+
+ML {*  
+  cterm_of @{theory} (regularise @{term "\<forall>x::trm. P x"} @{typ "trm"} @{term "RR"} @{context});
+  cterm_of @{theory} (my_reg @{term "RR"} @{term "\<forall>x::trm. P x"})
+*}
+
+ML {*  
+  cterm_of @{theory} (regularise @{term "\<exists>x::trm. P x"} @{typ "trm"} @{term "RR"} @{context});
+  cterm_of @{theory} (my_reg @{term "RR"} @{term "\<exists>x::trm. P x"})
+*}
+
+(* my version is not eta-expanded, but that should be OK *)
+ML {*  
+  cterm_of @{theory} (regularise @{term "All (P::trm \<Rightarrow> bool)"} @{typ "trm"} @{term "RR"} @{context});
+  cterm_of @{theory} (my_reg @{term "RR"} @{term "All (P::trm \<Rightarrow> bool)"})
+*}
+
+(*fun prove_reg trm \<Rightarrow> thm (we might need some facts to do this)
+  trm == new_trm
+*)
+
+section {* TRANSCONV *}
+
+
+ML {*
+fun build_goal_term lthy thm constructors rty qty =
+  let
+    fun mk_rep tm =
+      let
+        val ty = exchange_ty rty qty (fastype_of tm)
+      in fst (get_fun repF rty qty lthy ty) $ tm end
+
+    fun mk_abs tm =
+      let
+        val _ = tracing (Syntax.string_of_term @{context} tm)
+        val _ = tracing (Syntax.string_of_typ @{context} (fastype_of tm))
+        val ty = exchange_ty rty qty (fastype_of tm) in
+      fst (get_fun absF rty qty lthy ty) $ tm end
+
+    fun is_constructor (Const (x, _)) = member (op =) constructors x
+      | is_constructor _ = false;
+
+    fun build_aux lthy tm =
+      case tm of
+      Abs (a as (_, vty, _)) =>
+      let
+        val (vs, t) = Term.dest_abs a;
+        val v = Free(vs, vty);
+        val t' = lambda v (build_aux lthy t)
+      in
+      if (not (needs_lift rty (fastype_of tm))) then t'
+      else mk_rep (mk_abs (
+        if not (needs_lift rty vty) then t'
+        else
+          let
+            val v' = mk_rep (mk_abs v);
+            val t1 = Envir.beta_norm (t' $ v')
+          in
+            lambda v t1
+          end
+      ))
+      end
+    | x =>
+      let
+        val _ = tracing (">>" ^ Syntax.string_of_term @{context} tm)
+        val (opp, tms0) = Term.strip_comb tm
+        val tms = map (build_aux lthy) tms0
+        val ty = fastype_of tm
+      in
+        if (((fst (Term.dest_Const opp)) = @{const_name Respects}) handle _ => false)
+          then (list_comb (opp, (hd tms0) :: (tl tms)))
+      else if (is_constructor opp andalso needs_lift rty ty) then
+          mk_rep (mk_abs (list_comb (opp,tms)))
+        else if ((Term.is_Free opp) andalso (length tms > 0) andalso (needs_lift rty ty)) then
+            mk_rep(mk_abs(list_comb(opp,tms)))
+        else if tms = [] then opp
+        else list_comb(opp, tms)
+      end
+  in
+    build_aux lthy (Thm.prop_of thm)
+  end
+*}
+
+ML {*
+fun build_goal ctxt thm cons rty qty =
+  Logic.mk_equals ((Thm.prop_of thm), (build_goal_term ctxt thm cons rty qty))
+*}
+
+
+
+
 
 text {* finite set example *}
 print_syntax
@@ -685,138 +1047,10 @@
 ML {* val tt = Type ("fun", [Type ("fun", [qty, @{typ "prop"}]), @{typ "prop"}]) *}
 ML {* val fall = Const(@{const_name all}, dummyT) *}
 
-ML {*
-fun needs_lift (rty as Type (rty_s, _)) ty =
-  case ty of
-    Type (s, tys) =>
-      (s = rty_s) orelse (exists (needs_lift rty) tys)
-  | _ => false
-
-*}
-
-ML {*
-fun build_goal_term lthy thm constructors rty qty =
-  let
-    fun mk_rep tm =
-      let
-        val ty = exchange_ty rty qty (fastype_of tm)
-      in fst (get_fun repF rty qty lthy ty) $ tm end
-
-    fun mk_abs tm =
-      let
-        val _ = tracing (Syntax.string_of_term @{context} tm)
-        val _ = tracing (Syntax.string_of_typ @{context} (fastype_of tm))
-        val ty = exchange_ty rty qty (fastype_of tm) in
-      fst (get_fun absF rty qty lthy ty) $ tm end
-
-    fun is_constructor (Const (x, _)) = member (op =) constructors x
-      | is_constructor _ = false;
+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 *}
 
-    fun build_aux lthy tm =
-      case tm of
-      Abs (a as (_, vty, _)) =>
-      let
-        val (vs, t) = Term.dest_abs a;
-        val v = Free(vs, vty);
-        val t' = lambda v (build_aux lthy t)
-      in
-      if (not (needs_lift rty (fastype_of tm))) then t'
-      else mk_rep (mk_abs (
-        if not (needs_lift rty vty) then t'
-        else
-          let
-            val v' = mk_rep (mk_abs v);
-            val t1 = Envir.beta_norm (t' $ v')
-          in
-            lambda v t1
-          end
-      ))
-      end
-    | x =>
-      let
-        val _ = tracing (">>" ^ Syntax.string_of_term @{context} tm)
-        val (opp, tms0) = Term.strip_comb tm
-        val tms = map (build_aux lthy) tms0
-        val ty = fastype_of tm
-      in
-        if (((fst (Term.dest_Const opp)) = @{const_name Respects}) handle _ => false)
-          then (list_comb (opp, (hd tms0) :: (tl tms)))
-      else if (is_constructor opp andalso needs_lift rty ty) then
-          mk_rep (mk_abs (list_comb (opp,tms)))
-        else if ((Term.is_Free opp) andalso (length tms > 0) andalso (needs_lift rty ty)) then
-            mk_rep(mk_abs(list_comb(opp,tms)))
-        else if tms = [] then opp
-        else list_comb(opp, tms)
-      end
-  in
-    build_aux lthy (Thm.prop_of thm)
-  end
 
-*}
-
-ML {*
-fun build_goal_term_old ctxt thm constructors rty qty mk_rep mk_abs =
-  let
-    fun mk_rep_abs x = mk_rep (mk_abs x);
-
-    fun is_constructor (Const (x, _)) = member (op =) constructors x
-      | is_constructor _ = false;
-
-    fun maybe_mk_rep_abs t =
-      let
-        val _ = writeln ("Maybe: " ^ Syntax.string_of_term ctxt t)
-      in
-        if fastype_of t = rty then mk_rep_abs t else t
-      end;
-
-    fun is_all (Const ("all", Type("fun", [Type("fun", [ty, _]), _]))) = ty = rty
-      | is_all _ = false;
-
-    fun is_ex (Const ("Ex", Type("fun", [Type("fun", [ty, _]), _]))) = ty = rty
-      | is_ex _ = false;
-
-    fun build_aux ctxt1 tm =
-      let
-        val (head, args) = Term.strip_comb tm;
-        val args' = map (build_aux ctxt1) args;
-      in
-        (case head of
-          Abs (x, T, t) =>
-            if T = rty then let
-              val ([x'], ctxt2) = Variable.variant_fixes [x] ctxt1;
-              val v = Free (x', qty);
-              val t' = subst_bound (mk_rep v, t);
-              val rec_term = build_aux ctxt2 t';
-              val _ = tracing (Syntax.string_of_term ctxt2 t')
-              val _ = tracing (Syntax.string_of_term ctxt2 (Term.lambda_name (x, v) rec_term))
-            in
-              Term.lambda_name (x, v) rec_term
-            end else let
-              val ([x'], ctxt2) = Variable.variant_fixes [x] ctxt1;
-              val v = Free (x', T);
-              val t' = subst_bound (v, t);
-              val rec_term = build_aux ctxt2 t';
-            in Term.lambda_name (x, v) rec_term end
-        | _ =>  (* I assume that we never lift 'prop' since it is not of sort type *)
-            if is_all head then
-              list_comb (Const(@{const_name all}, dummyT), args') |> Syntax.check_term ctxt1
-            else if is_ex head then
-              list_comb (Const(@{const_name Ex}, dummyT), args') |> Syntax.check_term ctxt1
-            else if is_constructor head then
-              maybe_mk_rep_abs (list_comb (head, map maybe_mk_rep_abs args'))
-            else
-              maybe_mk_rep_abs (list_comb (head, args'))
-        )
-      end;
-  in
-    build_aux ctxt (Thm.prop_of thm)
-  end
-*}
-
-ML {*
-fun build_goal ctxt thm cons rty qty =
-  Logic.mk_equals ((Thm.prop_of thm), (build_goal_term ctxt thm cons rty qty))
-*}
 
 ML {*
   val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm m2}))
@@ -825,66 +1059,8 @@
 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_goal_term_old @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"} mk_rep mk_abs)
-*}
-
-
-text {*
-  Unabs_def converts a definition given as
-
-    c \<equiv> %x. %y. f x y
-
-  to a theorem of the form
-
-    c x y \<equiv> f x y
-
-  This function is needed to rewrite the right-hand
-  side to the left-hand side.
 *}
 
-ML {*
-fun unabs_def ctxt def =
-let
-  val (lhs, rhs) = Thm.dest_equals (cprop_of def)
-  val xs = strip_abs_vars (term_of rhs)
-  val (_, ctxt') = Variable.add_fixes (map fst xs) ctxt
-
-  val thy = ProofContext.theory_of ctxt'
-  val cxs = map (cterm_of thy o Free) xs
-  val new_lhs = Drule.list_comb (lhs, cxs)
-
-  fun get_conv [] = Conv.rewr_conv def
-    | get_conv (x::xs) = Conv.fun_conv (get_conv xs)
-in
-  get_conv xs new_lhs |>
-  singleton (ProofContext.export ctxt' ctxt)
-end
-*}
-
-ML {* (* Test: *) @{thm IN_def}; unabs_def @{context} @{thm IN_def} *}
-
-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 *}
-
-lemma atomize_eqv[atomize]: 
-  shows "(Trueprop A \<equiv> Trueprop B) \<equiv> (A \<equiv> B)" 
-proof
-  assume "A \<equiv> B" 
-  then show "Trueprop A \<equiv> Trueprop B" by unfold
-next
-  assume *: "Trueprop A \<equiv> Trueprop B"
-  have "A = B"
-  proof (cases A)
-    case True
-    have "A" by fact
-    then show "A = B" using * by simp
-  next
-    case False
-    have "\<not>A" by fact
-    then show "A = B" using * by auto
-  qed
-  then show "A \<equiv> B" by (rule eq_reflection)
-qed
 
 (* Has all the theorems about fset plugged in. These should be parameters to the tactic *)
 ML {*
@@ -973,229 +1149,6 @@
   apply (tactic {* transconv_fset_tac' @{context} *})
   done
 
-section {* handling quantifiers - regularize *}
-
-text {* tyRel takes a type and builds a relation that a quantifier over this
-  type needs to respect. *}
-ML {*
-fun tyRel ty rty rel lthy =
-  if ty = rty 
-  then rel
-  else (case ty of
-          Type (s, tys) =>
-            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), map (fn ty => tyRel ty rty rel lthy) tys)
-             | NONE  => HOLogic.eq_const ty
-            )
-            end
-        | _ => HOLogic.eq_const ty)
-*}
-
-ML {*
-  cterm_of @{theory} (tyRel @{typ "trm \<Rightarrow> bool"} @{typ "trm"} @{term "RR"} @{context})
-*}
-
-definition
-  Babs :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
-where
-  "(x \<in> p) \<Longrightarrow> (Babs p m x = m x)"
-(* TODO: Consider defining it with an "if"; sth like:
-   Babs p m = \<lambda>x. if x \<in> p then m x else undefined
-*)
-
-ML {*
-(* trm \<Rightarrow> new_trm *)
-fun regularise trm rty rel lthy =
-  case trm of
-    Abs (x, T, t) =>
-      if (needs_lift rty T) then let
-        val ([x'], lthy2) = Variable.variant_fixes [x] lthy;
-        val v = Free (x', T);
-        val t' = subst_bound (v, t);
-        val rec_term = regularise t' rty rel lthy2;
-        val lam_term = Term.lambda_name (x, v) rec_term;
-        val sub_res_term = tyRel T rty rel lthy;
-        val respects = Const (@{const_name Respects}, (fastype_of sub_res_term) --> T --> @{typ bool});
-        val res_term = respects $ sub_res_term;
-        val ty = fastype_of trm;
-        val rabs = Const (@{const_name Babs}, (fastype_of res_term) --> ty --> ty);
-        val rabs_term = (rabs $ res_term) $ lam_term;
-      in
-        rabs_term
-      end else let
-        val ([x'], lthy2) = Variable.variant_fixes [x] lthy;
-        val v = Free (x', T);
-        val t' = subst_bound (v, t);
-        val rec_term = regularise t' rty rel lthy2;
-      in
-        Term.lambda_name (x, v) rec_term
-      end
-  | ((Const (@{const_name "All"}, at)) $ (Abs (x, T, t))) =>
-      if (needs_lift rty T) then let
-        val ([x'], lthy2) = Variable.variant_fixes [x] lthy;
-        val v = Free (x', T);
-        val t' = subst_bound (v, t);
-        val rec_term = regularise t' rty rel lthy2;
-        val lam_term = Term.lambda_name (x, v) rec_term;
-        val sub_res_term = tyRel T rty rel lthy;
-        val respects = Const (@{const_name Respects}, (fastype_of sub_res_term) --> T --> @{typ bool});
-        val res_term = respects $ sub_res_term;
-        val ty = fastype_of lam_term;
-        val rall = Const (@{const_name Ball}, (fastype_of res_term) --> ty --> @{typ bool});
-        val rall_term = (rall $ res_term) $ lam_term;
-      in
-        rall_term
-      end else let
-        val ([x'], lthy2) = Variable.variant_fixes [x] lthy;
-        val v = Free (x', T);
-        val t' = subst_bound (v, t);
-        val rec_term = regularise t' rty rel lthy2;
-        val lam_term = Term.lambda_name (x, v) rec_term
-      in
-        Const(@{const_name "All"}, at) $ lam_term
-      end
-  | ((Const (@{const_name "All"}, at)) $ P) =>
-      let
-        val (_, [al, _]) = dest_Type (fastype_of P);
-        val ([x], lthy2) = Variable.variant_fixes [""] lthy;
-        val v = (Free (x, al));
-        val abs = Term.lambda_name (x, v) (P $ v);
-      in regularise ((Const (@{const_name "All"}, at)) $ abs) rty rel lthy2 end
-  | ((Const (@{const_name "Ex"}, at)) $ (Abs (x, T, t))) =>
-      if (needs_lift rty T) then let
-        val ([x'], lthy2) = Variable.variant_fixes [x] lthy;
-        val v = Free (x', T);
-        val t' = subst_bound (v, t);
-        val rec_term = regularise t' rty rel lthy2;
-        val lam_term = Term.lambda_name (x, v) rec_term;
-        val sub_res_term = tyRel T rty rel lthy;
-        val respects = Const (@{const_name Respects}, (fastype_of sub_res_term) --> T --> @{typ bool});
-        val res_term = respects $ sub_res_term;
-        val ty = fastype_of lam_term;
-        val rall = Const (@{const_name Bex}, (fastype_of res_term) --> ty --> @{typ bool});
-        val rall_term = (rall $ res_term) $ lam_term;
-      in
-        rall_term
-      end else let
-        val ([x'], lthy2) = Variable.variant_fixes [x] lthy;
-        val v = Free (x', T);
-        val t' = subst_bound (v, t);
-        val rec_term = regularise t' rty rel lthy2;
-        val lam_term = Term.lambda_name (x, v) rec_term
-      in
-        Const(@{const_name "Ex"}, at) $ lam_term
-      end
-  | ((Const (@{const_name "Ex"}, at)) $ P) =>
-      let
-        val (_, [al, _]) = dest_Type (fastype_of P);
-        val ([x], lthy2) = Variable.variant_fixes [""] lthy;
-        val v = (Free (x, al));
-        val abs = Term.lambda_name (x, v) (P $ v);
-      in regularise ((Const (@{const_name "Ex"}, at)) $ abs) rty rel lthy2 end
-  | a $ b => (regularise a rty rel lthy) $ (regularise b rty rel lthy)
-  | _ => trm
-
-*}
-
-ML {*
-  cterm_of @{theory} (regularise @{term "\<lambda>x :: int. x"} @{typ "trm"} @{term "RR"} @{context});
-  cterm_of @{theory} (regularise @{term "\<lambda>x :: trm. x"} @{typ "trm"} @{term "RR"} @{context});
-  cterm_of @{theory} (regularise @{term "\<forall>x :: trm. P x"} @{typ "trm"} @{term "RR"} @{context});
-  cterm_of @{theory} (regularise @{term "\<exists>x :: trm. P x"} @{typ "trm"} @{term "RR"} @{context});
-  cterm_of @{theory} (regularise @{term "All (P :: trm \<Rightarrow> bool)"} @{typ "trm"} @{term "RR"} @{context});
-*}
-
-(* my version of regularise *)
-(****************************)
-
-(* some helper functions *)
-
-
-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})
-*}
-
-(* applies f to the subterm of an abstractions, otherwise to the given term *)
-ML {*
-fun apply_subt f trm =
-  case trm of
-    Abs (x, T, t) => Abs (x, T, f t)
-  | _ => f trm
-*}
-
-
-(* FIXME: assumes always the typ is qty! *)
-(* FIXME: if there are more than one quotient, then you have to look up the relation *)
-ML {*
-fun my_reg rel trm =
-  case trm of
-    Abs (x, T, t) =>
-       let 
-          val ty1 = fastype_of trm
-       in
-         (mk_babs ty1 T) $ (mk_resp T $ rel) $ (Abs (x, T, my_reg rel t))    
-       end
-  | Const (@{const_name "All"}, ty) $ t =>
-       let 
-          val ty1 = domain_type ty
-          val ty2 = domain_type ty1
-       in
-         (mk_ball ty1) $ (mk_resp ty2 $ rel) $ (apply_subt (my_reg rel) t)      
-       end
-  | Const (@{const_name "Ex"}, ty) $ t =>
-       let 
-          val ty1 = domain_type ty
-          val ty2 = domain_type ty1
-       in
-         (mk_bex ty1) $ (mk_resp ty2 $ rel) $ (apply_subt (my_reg rel) t)    
-       end
-  | t1 $ t2 => (my_reg rel t1) $ (my_reg rel t2)
-  | _ => trm
-*}
-
-ML {*  
-  cterm_of @{theory} (regularise @{term "\<lambda>x::trm. x"} @{typ "trm"} @{term "RR"} @{context});
-  cterm_of @{theory} (my_reg @{term "RR"} @{term "\<lambda>x::trm. x"})
-*}
-
-ML {*  
-  cterm_of @{theory} (regularise @{term "\<forall>(x::trm) (y::trm). P x y"} @{typ "trm"} @{term "RR"} @{context});
-  cterm_of @{theory} (my_reg @{term "RR"} @{term "\<forall>(x::trm) (y::trm). P x y"})
-*}
-
-ML {*  
-  cterm_of @{theory} (regularise @{term "\<forall>x::trm. P x"} @{typ "trm"} @{term "RR"} @{context});
-  cterm_of @{theory} (my_reg @{term "RR"} @{term "\<forall>x::trm. P x"})
-*}
-
-ML {*  
-  cterm_of @{theory} (regularise @{term "\<exists>x::trm. P x"} @{typ "trm"} @{term "RR"} @{context});
-  cterm_of @{theory} (my_reg @{term "RR"} @{term "\<exists>x::trm. P x"})
-*}
-
-(* my version is not eta-expanded, but that should be OK *)
-ML {*  
-  cterm_of @{theory} (regularise @{term "All (P::trm \<Rightarrow> bool)"} @{typ "trm"} @{term "RR"} @{context});
-  cterm_of @{theory} (my_reg @{term "RR"} @{term "All (P::trm \<Rightarrow> bool)"})
-*}
-
-ML {*
-fun atomize_thm thm =
-let
-  val thm' = forall_intr_vars thm
-  val thm'' = ObjectLogic.atomize (cprop_of thm')
-in
-  Simplifier.rewrite_rule [thm''] thm'
-end
-*}
 
 thm list.induct
 lemma list_induct_hol4:
@@ -1206,9 +1159,6 @@
 
 ML {* atomize_thm @{thm list_induct_hol4} *}
 
-(*fun prove_reg trm \<Rightarrow> thm (we might need some facts to do this)
-  trm == new_trm
-*)
 
 ML {* val li = Thm.freezeT (atomize_thm @{thm list_induct_hol4}) *}
 
@@ -1366,7 +1316,6 @@
 ML_prf {* val t = Thm.lift_rule (hd (cprems_of (Isar.goal ()))) @{thm "APPLY_RSP_II" } *}
 ML_prf {* Toplevel.program (fn () => cterm_instantiate insts t) *}
 
-ML_prf {* Toplevel.program (fn () => Drule.instantiate' [] [SOME f_abs_c, SOME f_abs_c] t) *}