
diff -r c13bb9e02eb7 -r 5f6ee943c697 QuotMain.thy
--- a/QuotMain.thy	Fri Aug 28 17:12:19 2009 +0200
+++ b/QuotMain.thy	Tue Sep 15 09:59:56 2009 +0200
@@ -108,11 +108,12 @@
 end
 *}
 
+(*
 ML {*
- typedef_term @{term R} @{typ "nat"} @{context} 
+ typedef_term @{term R} @{typ "nat"} @{context}
   |> Syntax.string_of_term @{context}
   |> writeln
-*}
+*}*)
 
 ML {*
 val typedef_tac =  
@@ -199,6 +200,13 @@
 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
@@ -208,7 +216,32 @@
 end
 *}
 
-ML {* 
+ML {*
+val no_vars = Thm.rule_attribute (fn context => fn th =>
+  let
+    val ctxt = Variable.set_body false (Context.proof_of context);
+    val ((_, [th']), _) = Variable.import true [th] ctxt;
+  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 *)
@@ -233,6 +266,11 @@
          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
@@ -241,29 +279,76 @@
   val quotient_thm = typedef_quotient_thm (rel, ABS, REP, ABS_def, REP_def, quot_thm) lthy''
   val quotient_thm_name = Binding.prefix_name "QUOTIENT_" qty_name
 
+  (* interpretation *)
+  val bindd = ((Binding.make ("", Position.none)), ([]: Attrib.src list))
+  val ((_, [eqn1pre]), lthy''') = Variable.import true [ABS_def] lthy'';
+  val eqn1i = Thm.prop_of (symmetric eqn1pre)
+  val ((_, [eqn2pre]), lthy'''') = Variable.import true [REP_def] lthy''';
+  val eqn2i = Thm.prop_of (symmetric eqn2pre)
+
+  val exp_morphism = ProofContext.export_morphism lthy'''' (ProofContext.init (ProofContext.theory_of lthy''''));
+  val exp_term = Morphism.term exp_morphism;
+  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"*))
+  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),
+    Expression.Named [
+     ("R", rel),
+     ("Abs", abs),
+     ("Rep", rep)
+    ]))]
 in
-  lthy'' 
-  |> reg_thm (quot_thm_name, quot_thm)  
+  lthy''''
+  |> reg_thm (quot_thm_name, quot_thm)
   ||>> reg_thm (quotient_thm_name, quotient_thm)
+  ||> LocalTheory.theory (fn thy =>
+      let
+        val global_eqns = map exp_term [eqn2i, eqn1i];
+        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" 
 | app  "trm" "trm"
 | lam  "nat" "trm"
 
-axiomatization R :: "trm \<Rightarrow> trm \<Rightarrow> bool" where
-  r_eq: "EQUIV R"
+axiomatization RR :: "trm \<Rightarrow> trm \<Rightarrow> bool" where
+  r_eq: "EQUIV RR"
 
 ML {*
   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 {*
-  typedef_main (@{binding "qtrm"}, @{term "R"}, @{typ trm}, @{thm r_eq}) #> snd
+  fn lthy =>
+    Toplevel.program (fn () =>
+    exception_trace (
+      fn () => snd (typedef_main (@{binding "qtrm"}, @{term "RR"}, @{typ trm}, @{thm r_eq}) lthy)
+    )
+  )
 *}
+print_theorems
+
+(*thm QUOT_TYPE_I_qtrm.thm11*)
+
 
 term Rep_qtrm
 term REP_qtrm
@@ -289,16 +374,22 @@
 consts R' :: "'a trm' \<Rightarrow> 'a trm' \<Rightarrow> bool"
 axioms r_eq': "EQUIV R'"
 
+
 local_setup {*
-  typedef_main (@{binding "qtrm'"}, @{term "R'"}, @{typ "'a trm'"}, @{thm r_eq'}) #> snd
+  fn lthy =>
+    exception_trace
+      (fn () => (typedef_main (@{binding "qtrm'"}, @{term "R'"}, @{typ "'a trm'"}, @{thm r_eq'}) #> snd) lthy)
 *}
 
+print_theorems
+
 term ABS_qtrm'
 term REP_qtrm'
 thm QUOT_TYPE_qtrm'
 thm QUOTIENT_qtrm'
 thm Rep_qtrm'
 
+
 text {* a test with lists of terms *}
 datatype t =
   vr "string"
@@ -387,7 +478,7 @@
 let
   val ty = fastype_of nconst
   val (arg_tys, res_ty) = strip_type ty
- 
+
   val fresh_args = arg_tys |> map (pair "x")
                            |> Variable.variant_frees lthy [nconst, oconst] 
                            |> map Free
@@ -439,7 +530,7 @@
 thm VR_def
 thm AP_def
 thm LM_def
-term LM 
+term LM
 term VR
 term AP
 
@@ -453,10 +544,12 @@
 consts Rt' :: "('a t') \<Rightarrow> ('a t') \<Rightarrow> bool"
 axioms t_eq': "EQUIV Rt'"
 
+
 local_setup {*
   typedef_main (@{binding "qt'"}, @{term "Rt'"}, @{typ "'a t'"}, @{thm t_eq'}) #> snd
 *}
 
+print_theorems
 
 local_setup {*
   make_const_def "VR'" @{term "vr'"} NoSyn @{typ "'a t'"} @{typ "'a qt'"} #> snd
@@ -473,13 +566,14 @@
 thm VR'_def
 thm AP'_def
 thm LM'_def
-term LM' 
+term LM'
 term VR'
 term AP'
 
+
 text {* finite set example *}
 print_syntax
-inductive 
+inductive
   list_eq (infix "\<approx>" 50)
 where
   "a#b#xs \<approx> b#a#xs"
@@ -505,6 +599,8 @@
   typedef_main (@{binding "fset"}, @{term "list_eq"}, @{typ "'a list"}, @{thm "equiv_list_eq"}) #> snd
 *}
 
+print_theorems
+
 typ "'a fset"
 thm "Rep_fset"
 
@@ -512,7 +608,7 @@
   make_const_def "EMPTY" @{term "[]"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
 *}
 
-term Nil 
+term Nil
 term EMPTY
 thm EMPTY_def
 
@@ -521,7 +617,7 @@
   make_const_def "INSERT" @{term "op #"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
 *}
 
-term Cons 
+term Cons
 term INSERT
 thm INSERT_def
 
@@ -543,38 +639,7 @@
 
 thm QUOTIENT_fset
 
-(* This code builds the interpretation from ML level, currently only
-   for fset *) 
-
-ML {* val mthd = Method.SIMPLE_METHOD (rtac @{thm QUOT_TYPE_fset} 1 THEN
-  simp_tac (HOL_basic_ss addsimps @{thms REP_fset_def [symmetric]}) 1 THEN
-  simp_tac (HOL_basic_ss addsimps @{thms ABS_fset_def [symmetric]}) 1) *}
-ML {* val mthdt = Method.Basic (fn _ => mthd) *}
-ML {* val bymt = Proof.global_terminal_proof (mthdt, NONE) *}
-ML {* val exp_i = [((Locale.intern @{theory} "QUOT_TYPE"),(("QUOT_TYPE_fset_i", true),
-  Expression.Named [
-   ("R",@{term list_eq}),
-   ("Abs",@{term Abs_fset}),
-   ("Rep",@{term Rep_fset})
-  ]))] *}
-ML {* val bindd = ((Binding.make ("",Position.none)),([]:Attrib.src list)) *}
-ML {* val eqn1i = (bindd, @{prop "QUOT_TYPE.ABS list_eq Abs_fset = ABS_fset"}) *}
-ML {* val eqn2i = (bindd, @{prop "QUOT_TYPE.REP Rep_fset = REP_fset"}) *}
-setup {* fn thy => ProofContext.theory_of
-  (bymt (Expression.interpretation (exp_i, []) [eqn2i,eqn1i] thy)) *}
-
-(* It is eqivalent to the below:
-
-interpretation QUOT_TYPE_fset_i: QUOT_TYPE list_eq Abs_fset Rep_fset
-  where "QUOT_TYPE.ABS list_eq Abs_fset = ABS_fset"
-    and "QUOT_TYPE.REP Rep_fset = REP_fset"
-  unfolding ABS_fset_def REP_fset_def
-  apply (rule QUOT_TYPE_fset)
-  apply (simp only: ABS_fset_def[symmetric])
-  apply (simp only: REP_fset_def[symmetric])
-  done
-*)
-
+thm QUOT_TYPE_I_fset.thm11
 
 
 fun
@@ -628,7 +693,7 @@
 unfolding IN_def EMPTY_def
 apply(rule_tac f="(op =) False" in arg_cong)
 apply(rule mem_respects)
-apply(simp only: QUOT_TYPE_fset_i.REP_ABS_rsp)
+apply(simp only: QUOT_TYPE_I_fset.REP_ABS_rsp)
 apply(rule list_eq.intros)
 done
 
@@ -654,7 +719,7 @@
 done
 
 lemma append_respects_fst:
-  assumes a : "list_eq l1 l2"  
+  assumes a : "list_eq l1 l2"
   shows "list_eq (l1 @ s) (l2 @ s)"
   using a
   apply(induct)
@@ -674,19 +739,19 @@
   unfolding UNION_def EMPTY_def INSERT_def
   apply(rule_tac f="(op &)" in arg_cong2)
   apply(rule_tac f="(op =)" in arg_cong2)
-  apply(simp only: QUOT_TYPE_fset_i.thm11[symmetric])
+  apply(simp only: QUOT_TYPE_I_fset.thm11[symmetric])
   apply(rule append_respects_fst)
-  apply(simp only:QUOT_TYPE_fset_i.REP_ABS_rsp)
+  apply(simp only:QUOT_TYPE_I_fset.REP_ABS_rsp)
   apply(rule list_eq_sym)
   apply(simp)
   apply(rule_tac f="(op =)" in arg_cong2)
-  apply(simp only: QUOT_TYPE_fset_i.thm11[symmetric])
+  apply(simp only: QUOT_TYPE_I_fset.thm11[symmetric])
   apply(rule append_respects_fst)
-  apply(simp only: QUOT_TYPE_fset_i.REP_ABS_rsp)
+  apply(simp only: QUOT_TYPE_I_fset.REP_ABS_rsp)
   apply(rule list_eq_sym)
-  apply(simp only: QUOT_TYPE_fset_i.thm11[symmetric])
+  apply(simp only: QUOT_TYPE_I_fset.thm11[symmetric])
   apply(rule list_eq.intros(5))
-  apply(simp only: QUOT_TYPE_fset_i.REP_ABS_rsp)
+  apply(simp only: QUOT_TYPE_I_fset.REP_ABS_rsp)
   apply(rule list_eq_sym)
 done
 
@@ -695,7 +760,7 @@
      (UNION EMPTY s = s) &
      ((UNION (INSERT e s1) s2) = (INSERT e (UNION s1 s2)))"
   apply (simp add: yyy)
-  apply (rule QUOT_TYPE_fset_i.thm10)
+  apply (rule QUOT_TYPE_I_fset.thm10)
   done
 
 ML {*
@@ -730,13 +795,6 @@
   HOLogic.mk_eq ((build_aux concl), concl)
 end *}
 
-ML {*
-val no_vars = Thm.rule_attribute (fn context => fn th =>
-  let
-    val ctxt = Variable.set_body false (Context.proof_of context);
-    val ((_, [th']), _) = Variable.import true [th] ctxt;
-  in th' end);
-*}
 
 ML {*
   val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm m1}))
@@ -756,7 +814,7 @@
 apply(rule_tac f="(op =)" in arg_cong2)
 unfolding IN_def EMPTY_def
 apply (rule_tac mem_respects)
-apply (simp only: QUOT_TYPE_fset_i.REP_ABS_rsp)
+apply (simp only: QUOT_TYPE_I_fset.REP_ABS_rsp)
 apply (simp_all)
 apply (rule list_eq_sym)
 done
@@ -786,13 +844,13 @@
 unfolding IN_def
 apply (rule_tac mem_respects)
 unfolding INSERT_def
-apply (simp only: QUOT_TYPE_fset_i.REP_ABS_rsp)
+apply (simp only: QUOT_TYPE_I_fset.REP_ABS_rsp)
 apply (rule cons_preserves)
-apply (simp only: QUOT_TYPE_fset_i.REP_ABS_rsp)
+apply (simp only: QUOT_TYPE_I_fset.REP_ABS_rsp)
 apply (rule list_eq_sym)
 apply(rule_tac f="(op \<or>)" in arg_cong2)
 apply (simp)
 apply (rule_tac mem_respects)
-apply (simp only: QUOT_TYPE_fset_i.REP_ABS_rsp)
+apply (simp only: QUOT_TYPE_I_fset.REP_ABS_rsp)
 apply (rule list_eq_sym)
 done




