# HG changeset patch # User Cezary Kaliszyk # Date 1253007095 -7200 # Node ID 06b158ee1545f9bff0c6850bf67e0aa453d53b83 # Parent f46eddb570a383a314d0bf41adfaf890be898f1f Code cleanup 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 \ 'a \ bool" and Abs :: "('a \ bool) \ 'b" @@ -90,11 +84,6 @@ section {* type definition for the quotient type *} ML {* -Variable.variant_frees -*} - - -ML {* (* constructs the term \(c::ty \ bool). \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)