# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1255514739 -7200
# Node ID 56ad69873907f6b02a14586434ffea5f947b685d
# Parent  bdcfb24461f847a3a8df8d65dea9c4127375b283
Fixed bug in regularise types. Now we can regularise list.induct.

diff -r bdcfb24461f8 -r 56ad69873907 QuotMain.thy
--- a/QuotMain.thy	Wed Oct 14 11:23:55 2009 +0200
+++ b/QuotMain.thy	Wed Oct 14 12:05:39 2009 +0200
@@ -364,7 +364,7 @@
         rabs_term
       end else let
         val ([x'], lthy2) = Variable.variant_fixes [x] lthy;
-        val v = Free (x', fastype_of t);
+        val v = Free (x', T);
         val t' = subst_bound (v, t);
         val rec_term = regularise t' rty rel lthy2;
       in
@@ -387,7 +387,7 @@
         rall_term
       end else let
         val ([x'], lthy2) = Variable.variant_fixes [x] lthy;
-        val v = Free (x', fastype_of t);
+        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
@@ -411,7 +411,7 @@
         rall_term
       end else let
         val ([x'], lthy2) = Variable.variant_fixes [x] lthy;
-        val v = Free (x', fastype_of t);
+        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
@@ -424,12 +424,15 @@
 *}
 
 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})
 *}
 
 
+
+
 ML {*
 fun atomize_thm thm =
 let
@@ -1127,18 +1130,22 @@
 
 ML {* val li = Thm.freezeT (atomize_thm @{thm list.induct}) *}
 
-ML {*
-Syntax.string_of_term @{context}  (regularise (prop_of li) @{typ "'a List.list"} @{term "op \<approx>"} @{context})
-|> writeln
-*}
-
-ML {*
-  Toplevel.program (fn () =>
-cterm_of @{theory} (regularise (prop_of li) @{typ "'a List.list"} @{term "op \<approx>"} @{context})
-  )
-*}
-
-
+prove {*
+ Logic.mk_equals
+   ((regularise (prop_of li) @{typ "'a List.list"} @{term "op \<approx>"} @{context}),
+   (prop_of li)) *}
+  apply (atomize(full))
+  apply (unfold Ball_def)
+  apply (tactic {* foo_tac' @{context} 1 *})
+  apply (simp only: IN_RESPECTS)
+  apply (simp_all add: expand_fun_eq)
+  prefer 2
+  apply (simp only: IN_RESPECTS)
+  apply (simp add:list_eq_refl)
+  apply (tactic {* foo_tac' @{context} 1 *})
+  prefer 2
+  apply (auto)
+  sorry
 
 ML {*
   val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm list.induct}))
@@ -1304,8 +1311,6 @@
 (*apply (simp only: FUN_MAP_I)*)
 apply (simp)
 apply (simp only: QUOT_TYPE_I_fset.thm10)
-apply (tactic {* foo_tac' @{context} 1 *})
-
 ..
 apply (simp add:IN_RESPECTS)