# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1251356679 -7200
# Node ID 0bc0db2e83f207c083613a2b4e38c67e304b8ec3
# Parent  b11b405b8271c1a033cfac97358301d22352bce4
Use metavariables in the 'non-lambda' definitions

diff -r b11b405b8271 -r 0bc0db2e83f2 QuotMain.thy
--- a/QuotMain.thy	Wed Aug 26 11:31:55 2009 +0200
+++ b/QuotMain.thy	Thu Aug 27 09:04:39 2009 +0200
@@ -592,24 +592,23 @@
 apply(auto)
 done
 
-ML {* 
-fun unlam_def t =
+ML {*
+fun unlam_def orig_ctxt ctxt t =
   let
     val (v, rest) = Thm.dest_abs NONE (Thm.rhs_of t)
-    val t2 = Drule.fun_cong_rule t v
+    val (vname, vt) = Term.dest_Free (Thm.term_of v)
+    val ([vnname], ctxt) = Variable.variant_fixes [vname] ctxt
+    val nv = Free(vnname, vt)
+    val t2 = Drule.fun_cong_rule t (Thm.cterm_of @{theory} nv)
     val tnorm = equal_elim (Drule.beta_eta_conversion (Thm.cprop_of t2)) t2
-  in unlam_def tnorm end
-  handle CTERM _ => t
+  in unlam_def orig_ctxt ctxt tnorm end
+  handle CTERM _ => singleton (ProofContext.export ctxt orig_ctxt) t
 *}
 
 local_setup {*
   make_const_def "IN" @{term "membship"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
 *}
 
-ML {* 
-  val IN_def = unlam_def @{thm IN_def}
-*}
-
 term membship
 term IN
 thm IN_def
@@ -694,7 +693,7 @@
 
 ML {*
   fun mk_rep_abs x = @{term REP_fset} $ (@{term ABS_fset} $ x)
-  val consts = [@{const_name "Nil"}]
+  val consts = [@{const_name "Nil"}, @{const_name "append"}, @{const_name "Cons"}]
 *}
 
 ML {*
@@ -704,8 +703,12 @@
       | is_const _ = false
     fun build_aux (Abs (s, t, tr)) = (Abs (s, t, build_aux tr))
       | build_aux (f $ a) =
-          (if is_const f then mk_rep_abs (f $ (build_aux a))
-          else ((build_aux f) $ (build_aux a)))
+          let
+            val (f,args) = strip_comb (f $ a)
+           in
+            (if is_const f then mk_rep_abs (list_comb (f, (map mk_rep_abs (map build_aux args))))
+            else list_comb ((build_aux f), (map build_aux args)))
+          end
       | build_aux x =
           if is_const x then mk_rep_abs x else x
     val concl = HOLogic.dest_Trueprop (Thm.concl_of thm)
@@ -730,7 +733,7 @@
 ML {* val emptyt = symmetric @{thm EMPTY_def} *}
 ML {* val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false [emptyt] cgoal) *}
 
-ML {* val in_t = (symmetric IN_def) *}
+ML {* val in_t = (symmetric (unlam_def @{context} @{context} @{thm IN_def})) *}
 ML {* val cgoal3 = Thm.rhs_of (MetaSimplifier.rewrite false [in_t] (cgoal2)) *}
 
 (*theorem "(IN x EMPTY = False) = (x memb [] = False)"*)
@@ -742,3 +745,15 @@
 apply (simp only: QUOT_TYPE_fset_i.REP_ABS_rsp)
 apply (simp_all)
 apply (rule list_eq_sym)
+done
+
+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 m1_novars consts mk_rep_abs
+  val cgoal = cterm_of @{theory} goal
+*}
+ML {* val uniont = symmetric (unlam_def @{context} @{context} @{thm UNION_def}) *}
+ML {* val cardt =  symmetric (unlam_def @{context} @{context} @{thm CARD_def}) *}
+ML {* val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true [cardt] cgoal) *}
+ML {* val cgoal3 = Thm.rhs_of (MetaSimplifier.rewrite true [uniont] cgoal2) *}