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 \ trm \ bool" where - r_eq: "EQUIV R" +axiomatization RR :: "trm \ trm \ 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' \ 'a trm' \ 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') \ ('a t') \ 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 "\" 50) where "a#b#xs \ 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 \)" 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