diff -r 8d0fad689dce -r e0b4bca46c6a QuotMain.thy --- a/QuotMain.thy Tue Aug 18 14:04:51 2009 +0200 +++ b/QuotMain.thy Thu Aug 20 10:31:44 2009 +0200 @@ -60,6 +60,12 @@ unfolding ABS_def by (simp only: equiv[simplified EQUIV_def] lem7) +lemma REP_ABS_rsp: + shows "R f g \ R f (REP (ABS g))" +apply(subst thm11) +apply(simp add: thm10 thm11) +done + lemma QUOTIENT: "QUOTIENT R ABS REP" apply(unfold QUOTIENT_def) @@ -74,6 +80,11 @@ 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 @@ -88,6 +99,12 @@ *} ML {* + typedef_term @{term R} @{typ "nat"} @{context} + |> Syntax.string_of_term @{context} + |> writeln +*} + +ML {* val typedef_tac = EVERY1 [rewrite_goal_tac @{thms mem_def}, rtac @{thm exI}, rtac @{thm exI}, rtac @{thm refl}] @@ -103,7 +120,7 @@ NONE typedef_tac) lthy *} -text {* proves the QUOTIENT theorem for the new type *} +text {* proves the QUOT_TYPE theorem for the new type *} ML {* fun typedef_quot_type_tac equiv_thm (typedef_info: Typedef.info) = let @@ -125,6 +142,11 @@ end *} +term QUOT_TYPE +ML {* HOLogic.mk_Trueprop *} +ML {* Goal.prove *} +ML {* Syntax.check_term *} + ML {* fun typedef_quot_type_thm (rel, abs, rep, equiv_thm, typedef_info) lthy = let @@ -225,16 +247,21 @@ consts R :: "trm \ trm \ bool" axioms r_eq: "EQUIV R" +ML {* + typedef_main +*} + local_setup {* typedef_main (@{binding "qtrm"}, @{term "R"}, @{typ trm}, @{thm r_eq}) #> snd *} term Rep_qtrm +term REP_qtrm term Abs_qtrm term ABS_qtrm -term REP_qtrm thm QUOT_TYPE_qtrm thm QUOTIENT_qtrm + thm Rep_qtrm text {* another test *} @@ -300,6 +327,7 @@ #> Context.theory_map (update @{type_name "fun"} {mapfun = @{const_name "fun_map"}}) *} + ML {* lookup (Context.Proof @{context}) @{type_name list} *} ML {* @@ -337,6 +365,14 @@ *} ML {* + get_fun rep @{typ t} @{typ qt} @{context} @{typ "t * nat"} + |> fst + |> Syntax.string_of_term @{context} + |> writeln +*} + + +ML {* fun get_const_def nconst oconst rty qty lthy = let val ty = fastype_of nconst @@ -378,6 +414,26 @@ end *} +local_setup {* + make_const_def "VR" @{term "vr"} NoSyn @{typ "t"} @{typ "qt"} #> snd +*} + +local_setup {* + make_const_def "AP" @{term "ap"} NoSyn @{typ "t"} @{typ "qt"} #> snd +*} + +local_setup {* + make_const_def "LM" @{term "lm"} NoSyn @{typ "t"} @{typ "qt"} #> snd +*} + +thm VR_def +thm AP_def +thm LM_def +term LM +term VR +term AP + + text {* a test with functions *} datatype 'a t' = vr' "string" @@ -391,6 +447,7 @@ typedef_main (@{binding "qt'"}, @{term "Rt'"}, @{typ "'a t'"}, @{thm t_eq'}) #> snd *} + local_setup {* make_const_def "VR'" @{term "vr'"} NoSyn @{typ "'a t'"} @{typ "'a qt'"} #> snd *} @@ -447,6 +504,8 @@ term Nil term EMPTY +thm EMPTY_def + local_setup {* make_const_def "INSERT" @{term "op #"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd @@ -454,6 +513,7 @@ term Cons term INSERT +thm INSERT_def local_setup {* make_const_def "UNION" @{term "op @"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd @@ -461,8 +521,9 @@ term append term UNION +thm UNION_def + thm QUOTIENT_fset -thm Insert_def fun membship :: "'a \ 'a list \ bool" ("_ memb _") @@ -470,6 +531,15 @@ m1: "(x memb []) = False" | m2: "(x memb (y#xs)) = ((x=y) \ (x memb xs))" +lemma mem_respects: + fixes z::"nat" + assumes a: "list_eq x y" + shows "z memb x = z memb y" +using a +apply(induct) +apply(auto) +done + local_setup {* make_const_def "IN" @{term "membship"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd @@ -477,78 +547,39 @@ term membship term IN - -lemma - shows "IN x EMPTY = False" -unfolding IN_def EMPTY_def -apply(auto) -thm Rep_fset_inverse +thm IN_def - - - - - - - +lemmas a = QUOT_TYPE.ABS_def[OF QUOT_TYPE_fset] +thm QUOT_TYPE.thm11[OF QUOT_TYPE_fset, THEN iffD1, simplified a] - -text {* old stuff *} - - -lemma QUOT_TYPE_qtrm_old: - "QUOT_TYPE R Abs_qtrm Rep_qtrm" -apply(rule QUOT_TYPE.intro) -apply(rule r_eq) -apply(rule Rep_qtrm[simplified mem_def]) -apply(rule Rep_qtrm_inverse) -apply(rule Abs_qtrm_inverse[simplified mem_def]) -apply(rule exI) -apply(rule refl) -apply(rule Rep_qtrm_inject) +lemma yy: + shows "(False = x memb []) = (False = IN (x::nat) EMPTY)" +unfolding IN_def EMPTY_def +apply(rule_tac f="(op =) False" in arg_cong) +apply(rule mem_respects) +apply(unfold REP_fset_def ABS_fset_def) +apply(rule QUOT_TYPE.REP_ABS_rsp[OF QUOT_TYPE_fset]) +apply(rule list_eq.intros) done -definition - "ABS_qtrm_old \ QUOT_TYPE.ABS R Abs_qtrm" - -definition - "REP_qtrm_old \ QUOT_TYPE.REP Rep_qtrm" - -lemma - "QUOTIENT R (ABS_qtrm) (REP_qtrm)" -apply(simp add: ABS_qtrm_def REP_qtrm_def) -apply(rule QUOT_TYPE.QUOTIENT) -apply(rule QUOT_TYPE_qtrm) +lemma + shows "IN (x::nat) EMPTY = False" +using m1 +apply - +apply(rule yy[THEN iffD1, symmetric]) +apply(simp) done -term "var" -term "app" -term "lam" - -definition - "VAR x \ ABS_qtrm (var x)" - -definition - "APP t1 t2 \ ABS_qtrm (app (REP_qtrm t1) (REP_qtrm t2))" - -definition - "LAM x t \ ABS_qtrm (lam x (REP_qtrm t))" - - - +lemma + shows "((x=y) \ (IN x xs) = (IN (x::nat) (INSERT y xs))) = + ((x = y) \ x memb REP_fset xs = x memb (y # REP_fset xs))" +unfolding IN_def INSERT_def +apply(rule_tac f="(op \) (x=y)" in arg_cong) +apply(rule_tac f="(op =) (x memb REP_fset xs)" in arg_cong) +apply(rule mem_respects) +apply(rule list_eq.intros(3)) +apply(unfold REP_fset_def ABS_fset_def) +apply(rule QUOT_TYPE.REP_ABS_rsp[OF QUOT_TYPE_fset]) +apply(rule list_eq_sym) +done -definition - "VR x \ ABS_qt (vr x)" - -definition - "AP ts \ ABS_qt (ap (map REP_qt ts))" - -definition - "LM x t \ ABS_qt (lm x (REP_qt t))" - -(* for printing types *) -ML {* -fun setmp_show_all_types f = - setmp show_all_types - (! show_types orelse ! show_sorts orelse ! show_all_types) f -*} \ No newline at end of file