
diff -r f46eddb570a3 -r 06b158ee1545 QuotMain.thy
--- a/QuotMain.thy	Tue Sep 15 10:00:34 2009 +0200
+++ b/QuotMain.thy	Tue Sep 15 11:31:35 2009 +0200
@@ -2,12 +2,6 @@
 imports QuotScript QuotList Prove
 begin
 
-(*
-prove {* @{prop "True"} *}
-apply(rule TrueI)
-done
-*)
-
 locale QUOT_TYPE =
   fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
   and   Abs :: "('a \<Rightarrow> bool) \<Rightarrow> 'b"
@@ -90,11 +84,6 @@
 section {* type definition for the quotient type *}
 
 ML {*
-Variable.variant_frees
-*}
-
-
-ML {*
 (* constructs the term \<lambda>(c::ty \<Rightarrow> bool). \<exists>x. c = rel x *)
 fun typedef_term rel ty lthy =
 let
@@ -200,19 +189,12 @@
 end
 *}
 
-(*
-locale foo = fixes x :: nat
-begin
-
-ML {* make_def (@{binding foo}, NoSyn, @{term "x + x"}) @{context} *}
-*)
-
 ML {*
 fun reg_thm (name, thm) lthy =
 let
   val ((_,[thm']), lthy') = LocalTheory.note Thm.theoremK ((name, []), [thm]) lthy
 in
-  (thm',lthy')
+  (thm', lthy')
 end
 *}
 
@@ -224,28 +206,11 @@
   in th' end);
 *}
 
-ML ProofContext.theory_of
-
-ML Expression.interpretation
-
-ML {*
-fun my_print_tac ctxt thm =
-let
-   val _ = tracing (Display.string_of_thm ctxt thm)
-in
-   Seq.single thm
-end *}
-
-ML LocalTheory.theory_result
-
-
-ML {* Binding.str_of @{binding foo} *}
-
 ML {*
 fun typedef_main (qty_name, rel, ty, equiv_thm) lthy =
 let
   (* generates typedef *)
-  val ((_,typedef_info), lthy') = typedef_make (qty_name, rel, ty) lthy
+  val ((_, typedef_info), lthy') = typedef_make (qty_name, rel, ty) lthy
 
   (* abs and rep functions *)
   val abs_ty = #abs_type typedef_info
@@ -266,11 +231,6 @@
          lthy' |> make_def (ABS_name, NoSyn, ABS_trm)
                ||>> make_def (REP_name, NoSyn, REP_trm)
 
-  (* REMOVE VARIFY *)
-  val _ = tracing (Syntax.string_of_typ lthy' (type_of ABS_trm))
-  val _ = tracing (Syntax.string_of_typ lthy' (type_of REP_trm))
-  val _ = tracing (Syntax.string_of_typ lthy' (type_of rel))
-
   (* quot_type theorem *)
   val quot_thm = typedef_quot_type_thm (rel, abs, rep, equiv_thm, typedef_info) lthy''
   val quot_thm_name = Binding.prefix_name "QUOT_TYPE_" qty_name
@@ -291,11 +251,10 @@
   val exp = Morphism.thm exp_morphism;
 
   val mthd = Method.SIMPLE_METHOD ((rtac quot_thm 1) THEN
-    ALLGOALS (simp_tac (HOL_basic_ss addsimps [(symmetric (exp ABS_def)), (symmetric (exp REP_def))]))
-    (*THEN print_tac "Hello"*))
+    ALLGOALS (simp_tac (HOL_basic_ss addsimps [(symmetric (exp ABS_def)), (symmetric (exp REP_def))])))
   val mthdt = Method.Basic (fn _ => mthd)
   val bymt = Proof.global_terminal_proof (mthdt, NONE)
-  val exp_i = [(@{const_name QUOT_TYPE},((("QUOT_TYPE_I_" ^ (Binding.name_of qty_name)), true),
+  val exp_i = [(@{const_name QUOT_TYPE}, ((("QUOT_TYPE_I_" ^ (Binding.name_of qty_name)), true),
     Expression.Named [
      ("R", rel),
      ("Abs", abs),
@@ -308,14 +267,13 @@
   ||> LocalTheory.theory (fn thy =>
       let
         val global_eqns = map exp_term [eqn2i, eqn1i];
+        (* Not sure if the following context should not be used *)
         val (global_eqns2, lthy''''') = Variable.import_terms true global_eqns lthy'''';
         val global_eqns3 = map (fn t => (bindd, t)) global_eqns2;
-(*        val _ = tracing (Syntax.string_of_typ lthy'''' (type_of (fst (Logic.dest_equals (exp_term eqn1i)))));*)
       in ProofContext.theory_of (bymt (Expression.interpretation (exp_i, []) global_eqns3 thy)) end)
 end
 *}
 
-
 section {* various tests for quotient types*}
 datatype trm =
   var  "nat"
@@ -329,26 +287,9 @@
   typedef_main
 *}
 
-(*ML {*
-  val lthy = @{context};
-  val qty_name = @{binding "qtrm"}
-  val rel = @{term "RR"}
-  val ty = @{typ trm}
-  val equiv_thm = @{thm r_eq}
-*}*)
-
 local_setup {*
-  fn lthy =>
-    Toplevel.program (fn () =>
-    exception_trace (
-      fn () => snd (typedef_main (@{binding "qtrm"}, @{term "RR"}, @{typ trm}, @{thm r_eq}) lthy)
-    )
-  )
+  typedef_main (@{binding "qtrm"}, @{term "RR"}, @{typ trm}, @{thm r_eq}) #> snd
 *}
-print_theorems
-
-(*thm QUOT_TYPE_I_qtrm.thm11*)
-
 
 term Rep_qtrm
 term REP_qtrm
@@ -357,6 +298,9 @@
 thm QUOT_TYPE_qtrm
 thm QUOTIENT_qtrm
 
+(* Test interpretation *)
+thm QUOT_TYPE_I_qtrm.thm11
+
 thm Rep_qtrm
 
 text {* another test *}
@@ -376,9 +320,7 @@
 
 
 local_setup {*
-  fn lthy =>
-    exception_trace
-      (fn () => (typedef_main (@{binding "qtrm'"}, @{term "R'"}, @{typ "'a trm'"}, @{thm r_eq'}) #> snd) lthy)
+  typedef_main (@{binding "qtrm'"}, @{term "R'"}, @{typ "'a trm'"}, @{thm r_eq'}) #> snd
 *}
 
 print_theorems
@@ -782,7 +724,7 @@
     fun build_aux (Abs (s, t, tr)) = (Abs (s, t, build_aux tr))
       | build_aux (f $ a) =
           let
-            val (f,args) = strip_comb (f $ a)
+            val (f, args) = strip_comb (f $ a)
             val _ = writeln (Syntax.string_of_term @{context} f)
            in
             (if is_const f then maybe_mk_rep_abs (list_comb (f, (map maybe_mk_rep_abs (map build_aux args))))
@@ -795,22 +737,20 @@
   HOLogic.mk_eq ((build_aux concl), concl)
 end *}
 
+ML {* val emptyt = (symmetric (unlam_def @{context} @{context} @{thm EMPTY_def})) *}
+ML {* val in_t = (symmetric (unlam_def @{context} @{context} @{thm IN_def})) *}
+ML {* val uniont = symmetric (unlam_def @{context} @{context} @{thm UNION_def}) *}
+ML {* val cardt =  symmetric (unlam_def @{context} @{context} @{thm CARD_def}) *}
+ML {* val insertt =  symmetric (unlam_def @{context} @{context} @{thm INSERT_def}) *}
 
 ML {*
   val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm m1}))
   val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs
   val cgoal = cterm_of @{theory} goal
+  val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false [emptyt, in_t] cgoal)
 *}
 
-ML {* val emptyt = symmetric @{thm EMPTY_def} *}
-ML {* val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false [emptyt] cgoal) *}
-
-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)"*)
-
-prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal3) *}
+prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal2) *}
 apply(rule_tac f="(op =)" in arg_cong2)
 unfolding IN_def EMPTY_def
 apply (rule_tac mem_respects)
@@ -824,22 +764,17 @@
   val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm length_append}))
   val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs
   val cgoal = cterm_of @{theory} goal
+  val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false [emptyt, in_t, cardt, uniont] cgoal)
 *}
-ML {* val uniont = symmetric (unlam_def @{context} @{context} @{thm UNION_def}) *}
-ML {* val cardt =  symmetric (unlam_def @{context} @{context} @{thm CARD_def}) *}
-ML {* val insertt =  symmetric (unlam_def @{context} @{context} @{thm INSERT_def}) *}
-ML {* val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true [cardt] cgoal) *}
-ML {* val cgoal3 = Thm.rhs_of (MetaSimplifier.rewrite true [uniont] cgoal2) *}
 
 thm m2
 ML {*
   val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm m2}))
   val goal = build_goal m1_novars consts @{typ "'a list"} mk_rep_abs
   val cgoal = cterm_of @{theory} goal
+  val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite false [emptyt, in_t, cardt, uniont, insertt] cgoal)
 *}
-ML {* val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true [in_t] cgoal) *}
-ML {* val cgoal3 = Thm.rhs_of (MetaSimplifier.rewrite true [insertt] cgoal2) *}
-prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal3) *}
+prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal2) *}
 apply(rule_tac f="(op =)" in arg_cong2)
 unfolding IN_def
 apply (rule_tac mem_respects)




