nominal2: comparison QuotMain.thy

equal deleted inserted replaced

-:8d0fad689dce
+:e0b4bca46c6a
 theorem thm11:
 shows "R r r' = (ABS r = ABS r')"
 unfolding ABS_def
 by (simp only: equiv[simplified EQUIV_def] lem7)
+lemma REP_ABS_rsp:
+shows "R f g \<Longrightarrow> R f (REP (ABS g))"
+apply(subst thm11)
+apply(simp add: thm10 thm11)
+done
 lemma QUOTIENT:
 "QUOTIENT R ABS REP"
 apply(unfold QUOTIENT_def)
 apply(simp add: thm10)
 apply(simp add: REP_refl)
 end
 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
 val [x, c] = [("x", ty), ("c", ty --> @{typ bool})]
 |> Variable.variant_frees lthy [rel]
 in
 lambda c
 (HOLogic.mk_exists
 ("x", ty, HOLogic.mk_eq (c, (rel $ x))))
 end
+*}
+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},
 (qty_name, map fst (Term.add_tfreesT ty []), NoSyn)
 (typedef_term rel ty lthy)
 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
 val rep_thm = #Rep typedef_info
 val rep_inv = #Rep_inverse typedef_info
 rtac rep_inv,
 rtac abs_inv_simpd, rtac @{thm exI}, rtac @{thm refl},
 rtac rep_inj]
 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
 val quot_type_const = Const (@{const_name "QUOT_TYPE"}, dummyT)
 | lam  "nat" "trm"
 consts R :: "trm \<Rightarrow> trm \<Rightarrow> 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 *}
 datatype 'a my = foo
 consts Rmy :: "'a my \<Rightarrow> 'a my \<Rightarrow> bool"
 setup {*
 Context.theory_map (update @{type_name "list"} {mapfun = @{const_name "map"}})
 #> Context.theory_map (update @{type_name "*"} {mapfun = @{const_name "prod_fun"}})
 #> Context.theory_map (update @{type_name "fun"}  {mapfun = @{const_name "fun_map"}})
 *}
 ML {* lookup (Context.Proof @{context}) @{type_name list} *}
 ML {*
 datatype abs_or_rep = abs | rep
 )
 end
 *}
 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
 val (arg_tys, res_ty) = strip_type ty
 in
 make_def (Binding.name nconst_name, mx, def_trm) lthy
 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"
 | ap' "('a t') * ('a t')"
 | lm' "'a" "string \<Rightarrow> ('a t')"
 axioms t_eq': "EQUIV Rt'"
 local_setup {*
 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
 *}
 make_const_def "EMPTY" @{term "[]"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
 *}
 term Nil
 term EMPTY
+thm EMPTY_def
 local_setup {*
 make_const_def "INSERT" @{term "op #"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
 *}
 term Cons
 term INSERT
+thm INSERT_def
 local_setup {*
 make_const_def "UNION" @{term "op @"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
 *}
 term append
 term UNION
+thm UNION_def
 thm QUOTIENT_fset
-thm Insert_def
 fun
 membship :: "'a \<Rightarrow> 'a list \<Rightarrow> bool" ("_ memb _")
 where
 m1: "(x memb []) = False"
 | m2: "(x memb (y#xs)) = ((x=y) \<or> (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
 *}
 term membship
 term IN
+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]
+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
 lemma
-shows "IN x EMPTY = False"
+shows "IN (x::nat) EMPTY = False"
-unfolding IN_def EMPTY_def
+using m1
-apply(auto)
+apply -
-thm Rep_fset_inverse
+apply(rule yy[THEN iffD1, symmetric])
+apply(simp)
+done
+lemma
+shows "((x=y) \<or> (IN x xs) = (IN (x::nat) (INSERT y xs))) =
+((x = y) \<or> x memb REP_fset xs = x memb (y # REP_fset xs))"
+unfolding IN_def INSERT_def
+apply(rule_tac f="(op \<or>) (x=y)" in arg_cong)
+apply(rule_tac f="(op =) (x memb REP_fset xs)" in arg_cong)
+apply(rule mem_respects)
-text {* old stuff *}
+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])
-lemma QUOT_TYPE_qtrm_old:
+apply(rule list_eq_sym)
-"QUOT_TYPE R Abs_qtrm Rep_qtrm"
+done
-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)
-done
-definition
-"ABS_qtrm_old \<equiv> QUOT_TYPE.ABS R Abs_qtrm"
-definition
-"REP_qtrm_old \<equiv> 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)
-done
-term "var"
-term "app"
-term "lam"
-definition
-"VAR x \<equiv> ABS_qtrm (var x)"
-definition
-"APP t1 t2 \<equiv> ABS_qtrm (app (REP_qtrm t1) (REP_qtrm t2))"
-definition
-"LAM x t \<equiv> ABS_qtrm (lam x (REP_qtrm t))"
-definition
-"VR x \<equiv> ABS_qt (vr x)"
-definition
-"AP ts \<equiv> ABS_qt (ap (map REP_qt ts))"
-definition
-"LM x t \<equiv> 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
-*}

changeset 2	e0b4bca46c6a
parent 1	8d0fad689dce
child 3	672e14609e6e