diff -r aeb4fc74984f -r 19e5aceb8c2d QuotMain.thy
--- a/QuotMain.thy	Thu Oct 15 11:20:50 2009 +0200
+++ b/QuotMain.thy	Thu Oct 15 11:25:25 2009 +0200
@@ -300,171 +300,6 @@
   |> writeln
 *}
 
-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 (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  => Const (@{const_name "op ="}, ty --> ty --> @{typ bool})
-            )
-            end
-        | _ => Const (@{const_name "op ="}, ty --> ty --> @{typ bool}))
-*}
-
-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});
-*}
-
-
-
-
-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
-ML {* atomize_thm @{thm list.induct} *}
-
-(*fun prove_reg trm \<Rightarrow> thm (we might need some facts to do this)
-  trm == new_trm
-*)
-
-
 text {* produces the definition for a lifted constant *}
 
 ML {*
@@ -1153,6 +988,175 @@
   apply (tactic {* foo_tac' @{context} 1 *})
   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 (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  => Const (@{const_name "op ="}, ty --> ty --> @{typ bool})
+            )
+            end
+        | _ => Const (@{const_name "op ="}, ty --> ty --> @{typ bool}))
+*}
+
+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});
+*}
+
+
+
+
+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
+ML {* atomize_thm @{thm list.induct} *}
+
+(*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}) *}
 
 prove {*
@@ -1251,7 +1255,7 @@
 local_setup {* lift_theorem_fset @{binding "leqi5_lift"} @{thm list_eq.intros(5)} *}
 local_setup {* lift_theorem_fset @{binding "m2_lift"} @{thm m2} *}
 thm card1_suc_r
-ML {* Toplevel.program (fn () => lift_theorem_fset @{binding "card_suc"} @{thm card1_suc_r} @{context}) *}
+(* ML {* Toplevel.program (fn () => lift_theorem_fset @{binding "card_suc"} @{thm card1_suc_r} @{context}) *}*)
 (*local_setup {* lift_theorem_fset @{binding "card_suc"} @{thm card1_suc} *}*)
 
 thm m1_lift