# HG changeset patch # User Christian Urban # Date 1260191390 -3600 # Node ID 8a1c8dc72b5cfe91950b34ef1cfe31614c6580ae # Parent 6088fea1c8b1e6aa87d85ae23e4d2694522fc093 directory re-arrangement diff -r 6088fea1c8b1 -r 8a1c8dc72b5c FSet.thy --- a/FSet.thy Mon Dec 07 14:00:36 2009 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,440 +0,0 @@ -theory FSet -imports QuotMain -begin - -inductive - list_eq (infix "\" 50) -where - "a#b#xs \ b#a#xs" -| "[] \ []" -| "xs \ ys \ ys \ xs" -| "a#a#xs \ a#xs" -| "xs \ ys \ a#xs \ a#ys" -| "\xs1 \ xs2; xs2 \ xs3\ \ xs1 \ xs3" - -lemma list_eq_refl: - shows "xs \ xs" - by (induct xs) (auto intro: list_eq.intros) - -lemma equivp_list_eq: - shows "equivp list_eq" - unfolding equivp_reflp_symp_transp reflp_def symp_def transp_def - apply(auto intro: list_eq.intros list_eq_refl) - done - -quotient fset = "'a list" / "list_eq" - apply(rule equivp_list_eq) - done - -print_theorems - -typ "'a fset" -thm "Rep_fset" -thm "ABS_fset_def" - -quotient_def - EMPTY :: "'a fset" -where - "EMPTY \ ([]::'a list)" - -term Nil -term EMPTY -thm EMPTY_def - -quotient_def - INSERT :: "'a \ 'a fset \ 'a fset" -where - "INSERT \ op #" - -term Cons -term INSERT -thm INSERT_def - -quotient_def - FUNION :: "'a fset \ 'a fset \ 'a fset" -where - "FUNION \ (op @)" - -term append -term FUNION -thm FUNION_def - -thm Quotient_fset - -thm QUOT_TYPE_I_fset.thm11 - - -fun - membship :: "'a \ 'a list \ bool" (infix "memb" 100) -where - m1: "(x memb []) = False" -| m2: "(x memb (y#xs)) = ((x=y) \ (x memb xs))" - -fun - card1 :: "'a list \ nat" -where - card1_nil: "(card1 []) = 0" -| card1_cons: "(card1 (x # xs)) = (if (x memb xs) then (card1 xs) else (Suc (card1 xs)))" - -quotient_def - CARD :: "'a fset \ nat" -where - "CARD \ card1" - -term card1 -term CARD -thm CARD_def - -(* text {* - Maybe make_const_def should require a theorem that says that the particular lifted function - respects the relation. With it such a definition would be impossible: - make_const_def @{binding CARD} @{term "length"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd -*}*) - -lemma card1_0: - fixes a :: "'a list" - shows "(card1 a = 0) = (a = [])" - by (induct a) auto - -lemma not_mem_card1: - fixes x :: "'a" - fixes xs :: "'a list" - shows "(~(x memb xs)) = (card1 (x # xs) = Suc (card1 xs))" - by auto - -lemma mem_cons: - fixes x :: "'a" - fixes xs :: "'a list" - assumes a : "x memb xs" - shows "x # xs \ xs" - using a by (induct xs) (auto intro: list_eq.intros ) - -lemma card1_suc: - fixes xs :: "'a list" - fixes n :: "nat" - assumes c: "card1 xs = Suc n" - shows "\a ys. ~(a memb ys) \ xs \ (a # ys)" - using c -apply(induct xs) -apply (metis Suc_neq_Zero card1_0) -apply (metis QUOT_TYPE_I_fset.R_trans card1_cons list_eq_refl mem_cons) -done - -definition - rsp_fold -where - "rsp_fold f = ((!u v. (f u v = f v u)) \ (!u v w. ((f u (f v w) = f (f u v) w))))" - -primrec - fold1 -where - "fold1 f (g :: 'a \ 'b) (z :: 'b) [] = z" -| "fold1 f g z (a # A) = - (if rsp_fold f - then ( - if (a memb A) then (fold1 f g z A) else (f (g a) (fold1 f g z A)) - ) else z)" - -lemma fs1_strong_cases: - fixes X :: "'a list" - shows "(X = []) \ (\a. \ Y. (~(a memb Y) \ (X \ a # Y)))" - apply (induct X) - apply (simp) - apply (metis QUOT_TYPE_I_fset.thm11 list_eq_refl mem_cons m1) - done - -quotient_def - IN :: "'a \ 'a fset \ bool" -where - "IN \ membship" - -term membship -term IN -thm IN_def - -term fold1 -quotient_def - FOLD :: "('a \ 'a \ 'a) \ ('b \ 'a) \ 'a \ 'b fset \ 'a" -where - "FOLD \ fold1" - -term fold1 -term fold -thm fold_def - -quotient_def - fmap::"('a \ 'b) \ 'a fset \ 'b fset" -where - "fmap \ map" - -term map -term fmap -thm fmap_def - -lemma memb_rsp: - fixes z - assumes a: "x \ y" - shows "(z memb x) = (z memb y)" - using a by induct auto - -lemma ho_memb_rsp[quotient_rsp]: - "(op = ===> (op \ ===> op =)) (op memb) (op memb)" - by (simp add: memb_rsp) - -lemma card1_rsp: - fixes a b :: "'a list" - assumes e: "a \ b" - shows "card1 a = card1 b" - using e by induct (simp_all add:memb_rsp) - -lemma ho_card1_rsp[quotient_rsp]: - "(op \ ===> op =) card1 card1" - by (simp add: card1_rsp) - -lemma cons_rsp[quotient_rsp]: - fixes z - assumes a: "xs \ ys" - shows "(z # xs) \ (z # ys)" - using a by (rule list_eq.intros(5)) - -lemma ho_cons_rsp[quotient_rsp]: - "(op = ===> op \ ===> op \) op # op #" - by (simp add: cons_rsp) - -lemma append_rsp_fst: - assumes a : "l1 \ l2" - shows "(l1 @ s) \ (l2 @ s)" - using a - by (induct) (auto intro: list_eq.intros list_eq_refl) - -lemma append_end: - shows "(e # l) \ (l @ [e])" - apply (induct l) - apply (auto intro: list_eq.intros list_eq_refl) - done - -lemma rev_rsp: - shows "a \ rev a" - apply (induct a) - apply simp - apply (rule list_eq_refl) - apply simp_all - apply (rule list_eq.intros(6)) - prefer 2 - apply (rule append_rsp_fst) - apply assumption - apply (rule append_end) - done - -lemma append_sym_rsp: - shows "(a @ b) \ (b @ a)" - apply (rule list_eq.intros(6)) - apply (rule append_rsp_fst) - apply (rule rev_rsp) - apply (rule list_eq.intros(6)) - apply (rule rev_rsp) - apply (simp) - apply (rule append_rsp_fst) - apply (rule list_eq.intros(3)) - apply (rule rev_rsp) - done - -lemma append_rsp: - assumes a : "l1 \ r1" - assumes b : "l2 \ r2 " - shows "(l1 @ l2) \ (r1 @ r2)" - apply (rule list_eq.intros(6)) - apply (rule append_rsp_fst) - using a apply (assumption) - apply (rule list_eq.intros(6)) - apply (rule append_sym_rsp) - apply (rule list_eq.intros(6)) - apply (rule append_rsp_fst) - using b apply (assumption) - apply (rule append_sym_rsp) - done - -lemma ho_append_rsp[quotient_rsp]: - "(op \ ===> op \ ===> op \) op @ op @" - by (simp add: append_rsp) - -lemma map_rsp: - assumes a: "a \ b" - shows "map f a \ map f b" - using a - apply (induct) - apply(auto intro: list_eq.intros) - done - -lemma ho_map_rsp[quotient_rsp]: - "(op = ===> op \ ===> op \) map map" - by (simp add: map_rsp) - -lemma map_append: - "(map f (a @ b)) \ (map f a) @ (map f b)" - by simp (rule list_eq_refl) - -lemma ho_fold_rsp[quotient_rsp]: - "(op = ===> op = ===> op = ===> op \ ===> op =) fold1 fold1" - apply (auto) - apply (case_tac "rsp_fold x") - prefer 2 - apply (erule_tac list_eq.induct) - apply (simp_all) - apply (erule_tac list_eq.induct) - apply (simp_all) - apply (auto simp add: memb_rsp rsp_fold_def) -done - -lemma list_equiv_rsp[quotient_rsp]: - shows "(op \ ===> op \ ===> op =) op \ op \" -by (auto intro: list_eq.intros) - -print_quotients - -ML {* val qty = @{typ "'a fset"} *} -ML {* val rsp_thms = - @{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp ho_map_rsp ho_append_rsp ho_fold_rsp} *} - -ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} -ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "fset"; *} -ML {* fun lift_tac_fset lthy t = lift_tac lthy t *} - -lemma "IN x EMPTY = False" -apply(tactic {* procedure_tac @{context} @{thm m1} 1 *}) -apply(tactic {* regularize_tac @{context} 1 *}) -apply(tactic {* all_inj_repabs_tac @{context} [rel_refl] [trans2] 1 *}) -apply(tactic {* clean_tac @{context} 1*}) -done - -lemma "IN x (INSERT y xa) = (x = y \ IN x xa)" -by (tactic {* lift_tac_fset @{context} @{thm m2} 1 *}) - -lemma "INSERT a (INSERT a x) = INSERT a x" -apply (tactic {* lift_tac_fset @{context} @{thm list_eq.intros(4)} 1 *}) -done - -lemma "x = xa \ INSERT a x = INSERT a xa" -apply (tactic {* lift_tac_fset @{context} @{thm list_eq.intros(5)} 1 *}) -done - -lemma "CARD x = Suc n \ (\a b. \ IN a b & x = INSERT a b)" -apply (tactic {* lift_tac_fset @{context} @{thm card1_suc} 1 *}) -done - -lemma "(\ IN x xa) = (CARD (INSERT x xa) = Suc (CARD xa))" -apply (tactic {* lift_tac_fset @{context} @{thm not_mem_card1} 1 *}) -done - -lemma "FOLD f g (z::'b) (INSERT a x) = - (if rsp_fold f then if IN a x then FOLD f g z x else f (g a) (FOLD f g z x) else z)" -apply(tactic {* lift_tac_fset @{context} @{thm fold1.simps(2)} 1 *}) -done - -ML {* fun inj_repabs_tac_fset lthy = inj_repabs_tac lthy [rel_refl] [trans2] *} - -lemma "fmap f (FUNION (x::'b fset) (xa::'b fset)) = FUNION (fmap f x) (fmap f xa)" -apply (tactic {* lift_tac_fset @{context} @{thm map_append} 1 *}) -done - -lemma "FUNION (FUNION x xa) xb = FUNION x (FUNION xa xb)" -apply (tactic {* lift_tac_fset @{context} @{thm append_assoc} 1 *}) -done - - -lemma "\P EMPTY; \a x. P x \ P (INSERT a x)\ \ P l" -apply (tactic {* (ObjectLogic.full_atomize_tac THEN' gen_frees_tac @{context}) 1 *}) -apply(tactic {* procedure_tac @{context} @{thm list.induct} 1 *}) -apply(tactic {* regularize_tac @{context} 1 *}) -defer -apply(tactic {* clean_tac @{context} 1 *}) -apply(tactic {* inj_repabs_tac_fset @{context} 1*})+ -done - -lemma list_induct_part: - assumes a: "P (x :: 'a list) ([] :: 'c list)" - assumes b: "\e t. P x t \ P x (e # t)" - shows "P x l" - apply (rule_tac P="P x" in list.induct) - apply (rule a) - apply (rule b) - apply (assumption) - done - -ML {* quot *} -thm quotient_thm - -lemma "P (x :: 'a list) (EMPTY :: 'c fset) \ (\e t. P x t \ P x (INSERT e t)) \ P x l" -apply (tactic {* lift_tac_fset @{context} @{thm list_induct_part} 1 *}) -done - -lemma "P (x :: 'a fset) (EMPTY :: 'c fset) \ (\e t. P x t \ P x (INSERT e t)) \ P x l" -apply (tactic {* lift_tac_fset @{context} @{thm list_induct_part} 1 *}) -done - -lemma "P (x :: 'a fset) ([] :: 'c list) \ (\e t. P x t \ P x (e # t)) \ P x l" -apply (tactic {* lift_tac_fset @{context} @{thm list_induct_part} 1 *}) -done - -quotient fset2 = "'a list" / "list_eq" - apply(rule equivp_list_eq) - done - -quotient_def - EMPTY2 :: "'a fset2" -where - "EMPTY2 \ ([]::'a list)" - -quotient_def - INSERT2 :: "'a \ 'a fset2 \ 'a fset2" -where - "INSERT2 \ op #" - -ML {* val quot = @{thms Quotient_fset Quotient_fset2} *} -ML {* fun inj_repabs_tac_fset lthy = inj_repabs_tac lthy [rel_refl] [trans2] *} -ML {* fun lift_tac_fset lthy t = lift_tac lthy t *} - -lemma "P (x :: 'a fset2) (EMPTY :: 'c fset) \ (\e t. P x t \ P x (INSERT e t)) \ P x l" -apply (tactic {* lift_tac_fset @{context} @{thm list_induct_part} 1 *}) -done - -lemma "P (x :: 'a fset) (EMPTY2 :: 'c fset2) \ (\e t. P x t \ P x (INSERT2 e t)) \ P x l" -apply (tactic {* lift_tac_fset @{context} @{thm list_induct_part} 1 *}) -done - -quotient_def - fset_rec::"'a \ ('b \ 'b fset \ 'a \ 'a) \ 'b fset \ 'a" -where - "fset_rec \ list_rec" - -quotient_def - fset_case::"'a \ ('b \ 'b fset \ 'a) \ 'b fset \ 'a" -where - "fset_case \ list_case" - -(* Probably not true without additional assumptions about the function *) -lemma list_rec_rsp[quotient_rsp]: - "(op = ===> (op = ===> op \ ===> op =) ===> op \ ===> op =) list_rec list_rec" - apply (auto) - apply (erule_tac list_eq.induct) - apply (simp_all) - sorry - -lemma list_case_rsp[quotient_rsp]: - "(op = ===> (op = ===> op \ ===> op =) ===> op \ ===> op =) list_case list_case" - apply (auto) - sorry - -ML {* val rsp_thms = @{thms list_rec_rsp list_case_rsp} @ rsp_thms *} -ML {* fun lift_tac_fset lthy t = lift_tac lthy t *} - -lemma "fset_rec (f1::'t) x (INSERT a xa) = x a xa (fset_rec f1 x xa)" -apply (tactic {* lift_tac_fset @{context} @{thm list.recs(2)} 1 *}) -done - -lemma "fset_case (f1::'t) f2 (INSERT a xa) = f2 a xa" -apply (tactic {* lift_tac_fset @{context} @{thm list.cases(2)} 1 *}) -done - - -end diff -r 6088fea1c8b1 -r 8a1c8dc72b5c IntEx.thy --- a/IntEx.thy Mon Dec 07 14:00:36 2009 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,276 +0,0 @@ -theory IntEx -imports QuotMain -begin - -fun - intrel :: "(nat \ nat) \ (nat \ nat) \ bool" (infix "\" 50) -where - "intrel (x, y) (u, v) = (x + v = u + y)" - -quotient my_int = "nat \ nat" / intrel - apply(unfold equivp_def) - apply(auto simp add: mem_def expand_fun_eq) - done - -thm quotient_equiv - -thm quotient_thm - -thm my_int_equivp - -print_theorems -print_quotients - -quotient_def - ZERO::"my_int" -where - "ZERO \ (0::nat, 0::nat)" - -ML {* print_qconstinfo @{context} *} - -term ZERO -thm ZERO_def - -ML {* prop_of @{thm ZERO_def} *} - -ML {* separate *} - -quotient_def - ONE::"my_int" -where - "ONE \ (1::nat, 0::nat)" - -ML {* print_qconstinfo @{context} *} - -term ONE -thm ONE_def - -fun - my_plus :: "(nat \ nat) \ (nat \ nat) \ (nat \ nat)" -where - "my_plus (x, y) (u, v) = (x + u, y + v)" - -quotient_def - PLUS::"my_int \ my_int \ my_int" -where - "PLUS \ my_plus" - -term my_plus -term PLUS -thm PLUS_def - -fun - my_neg :: "(nat \ nat) \ (nat \ nat)" -where - "my_neg (x, y) = (y, x)" - -quotient_def - NEG::"my_int \ my_int" -where - "NEG \ my_neg" - -term NEG -thm NEG_def - -definition - MINUS :: "my_int \ my_int \ my_int" -where - "MINUS z w = PLUS z (NEG w)" - -fun - my_mult :: "(nat \ nat) \ (nat \ nat) \ (nat \ nat)" -where - "my_mult (x, y) (u, v) = (x*u + y*v, x*v + y*u)" - -quotient_def - MULT::"my_int \ my_int \ my_int" -where - "MULT \ my_mult" - -term MULT -thm MULT_def - -(* NOT SURE WETHER THIS DEFINITION IS CORRECT *) -fun - my_le :: "(nat \ nat) \ (nat \ nat) \ bool" -where - "my_le (x, y) (u, v) = (x+v \ u+y)" - -quotient_def - LE :: "my_int \ my_int \ bool" -where - "LE \ my_le" - -term LE -thm LE_def - - -definition - LESS :: "my_int \ my_int \ bool" -where - "LESS z w = (LE z w \ z \ w)" - -term LESS -thm LESS_def - -definition - ABS :: "my_int \ my_int" -where - "ABS i = (if (LESS i ZERO) then (NEG i) else i)" - -definition - SIGN :: "my_int \ my_int" -where - "SIGN i = (if i = ZERO then ZERO else if (LESS ZERO i) then ONE else (NEG ONE))" - -ML {* print_qconstinfo @{context} *} - -lemma plus_sym_pre: - shows "my_plus a b \ my_plus b a" - apply(cases a) - apply(cases b) - apply(auto) - done - -lemma plus_rsp[quotient_rsp]: - shows "(intrel ===> intrel ===> intrel) my_plus my_plus" -by (simp) - -ML {* val qty = @{typ "my_int"} *} -ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} -ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "my_int"; *} - -ML {* fun lift_tac_intex lthy t = lift_tac lthy t *} - -ML {* fun inj_repabs_tac_intex lthy = inj_repabs_tac lthy [rel_refl] [trans2] *} -ML {* fun all_inj_repabs_tac_intex lthy = all_inj_repabs_tac lthy [rel_refl] [trans2] *} - -lemma test1: "my_plus a b = my_plus a b" -apply(rule refl) -done - -lemma "PLUS a b = PLUS a b" -apply(tactic {* procedure_tac @{context} @{thm test1} 1 *}) -apply(tactic {* regularize_tac @{context} 1 *}) -apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) -apply(tactic {* clean_tac @{context} 1 *}) -done - -thm lambda_prs - -lemma test2: "my_plus a = my_plus a" -apply(rule refl) -done - -lemma "PLUS a = PLUS a" -apply(tactic {* procedure_tac @{context} @{thm test2} 1 *}) -apply(rule ballI) -apply(rule apply_rsp[OF Quotient_my_int plus_rsp]) -apply(simp only: in_respects) -apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) -apply(tactic {* clean_tac @{context} 1 *}) -done - -lemma test3: "my_plus = my_plus" -apply(rule refl) -done - -lemma "PLUS = PLUS" -apply(tactic {* procedure_tac @{context} @{thm test3} 1 *}) -apply(rule plus_rsp) -apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) -apply(tactic {* clean_tac @{context} 1 *}) -done - - -lemma "PLUS a b = PLUS b a" -apply(tactic {* procedure_tac @{context} @{thm plus_sym_pre} 1 *}) -apply(tactic {* regularize_tac @{context} 1 *}) -apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) -apply(tactic {* clean_tac @{context} 1 *}) -done - -lemma plus_assoc_pre: - shows "my_plus (my_plus i j) k \ my_plus i (my_plus j k)" - apply (cases i) - apply (cases j) - apply (cases k) - apply (simp) - done - -lemma plus_assoc: "PLUS (PLUS x xa) xb = PLUS x (PLUS xa xb)" -apply(tactic {* procedure_tac @{context} @{thm plus_assoc_pre} 1 *}) -apply(tactic {* regularize_tac @{context} 1 *}) -apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) -apply(tactic {* clean_tac @{context} 1 *}) -done - -lemma ho_tst: "foldl my_plus x [] = x" -apply simp -done - -lemma "foldl PLUS x [] = x" -apply(tactic {* procedure_tac @{context} @{thm ho_tst} 1 *}) -apply(tactic {* regularize_tac @{context} 1 *}) -apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) -apply(tactic {* clean_tac @{context} 1 *}) -apply(simp only: foldl_prs[OF Quotient_my_int Quotient_my_int] nil_prs[OF Quotient_my_int]) -done - -lemma ho_tst2: "foldl my_plus x (h # t) \ my_plus h (foldl my_plus x t)" -sorry - -lemma "foldl PLUS x (h # t) = PLUS h (foldl PLUS x t)" -apply(tactic {* procedure_tac @{context} @{thm ho_tst2} 1 *}) -apply(tactic {* regularize_tac @{context} 1 *}) -apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) -apply(tactic {* clean_tac @{context} 1 *}) -apply(simp only: foldl_prs[OF Quotient_my_int Quotient_my_int] cons_prs[OF Quotient_my_int]) -done - -lemma ho_tst3: "foldl f (s::nat \ nat) ([]::(nat \ nat) list) = s" -by simp - -lemma "foldl f (x::my_int) ([]::my_int list) = x" -apply(tactic {* procedure_tac @{context} @{thm ho_tst3} 1 *}) -apply(tactic {* regularize_tac @{context} 1 *}) -apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) -(* TODO: does not work when this is added *) -(* apply(tactic {* lambda_prs_tac @{context} 1 *})*) -apply(tactic {* clean_tac @{context} 1 *}) -apply(simp only: foldl_prs[OF Quotient_my_int Quotient_my_int] nil_prs[OF Quotient_my_int]) -done - -lemma lam_tst: "(\x. (x, x)) y = (y, (y :: nat \ nat))" -by simp - -lemma "(\x. (x, x)) (y::my_int) = (y, y)" -apply(tactic {* procedure_tac @{context} @{thm lam_tst} 1 *}) -apply(tactic {* regularize_tac @{context} 1 *}) -apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) -apply(tactic {* clean_tac @{context} 1 *}) -apply(simp add: pair_prs) -done - -lemma lam_tst2: "(\(y :: nat \ nat). y) = (\(x :: nat \ nat). x)" -by simp - - - - -lemma "(\(y :: my_int). y) = (\(x :: my_int). x)" -apply(tactic {* procedure_tac @{context} @{thm lam_tst2} 1 *}) -defer -apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) -(*apply(tactic {* lambda_prs_tac @{context} 1 *})*) -sorry - -lemma lam_tst3: "(\(y :: nat \ nat \ nat \ nat). y) = (\(x :: nat \ nat \ nat \ nat). x)" -by auto - -lemma "(\(y :: my_int \ my_int). y) = (\(x :: my_int \ my_int). x)" -apply(tactic {* procedure_tac @{context} @{thm lam_tst3} 1 *}) -defer -apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) -apply(tactic {* lambda_prs_tac @{context} 1 *}) -sorry diff -r 6088fea1c8b1 -r 8a1c8dc72b5c IntEx2.thy --- a/IntEx2.thy Mon Dec 07 14:00:36 2009 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,436 +0,0 @@ -theory IntEx2 -imports QuotMain -uses - ("Tools/numeral.ML") - ("Tools/numeral_syntax.ML") - ("Tools/int_arith.ML") -begin - - -fun - intrel :: "(nat \ nat) \ (nat \ nat) \ bool" (infix "\" 50) -where - "intrel (x, y) (u, v) = (x + v = u + y)" - -quotient int = "nat \ nat" / intrel - apply(unfold equivp_def) - apply(auto simp add: mem_def expand_fun_eq) - done - -instantiation int :: "{zero, one, plus, minus, uminus, times, ord, abs, sgn}" -begin - -quotient_def - zero_qnt::"int" -where - "zero_qnt \ (0::nat, 0::nat)" - -definition Zero_int_def[code del]: - "0 = zero_qnt" - -quotient_def - one_qnt::"int" -where - "one_qnt \ (1::nat, 0::nat)" - -definition One_int_def[code del]: - "1 = one_qnt" - -fun - plus_raw :: "(nat \ nat) \ (nat \ nat) \ (nat \ nat)" -where - "plus_raw (x, y) (u, v) = (x + u, y + v)" - -quotient_def - plus_qnt::"int \ int \ int" -where - "plus_qnt \ plus_raw" - -definition add_int_def[code del]: - "z + w = plus_qnt z w" - -fun - minus_raw :: "(nat \ nat) \ (nat \ nat)" -where - "minus_raw (x, y) = (y, x)" - -quotient_def - minus_qnt::"int \ int" -where - "minus_qnt \ minus_raw" - -definition minus_int_def [code del]: - "- z = minus_qnt z" - -definition - diff_int_def [code del]: "z - w = z + (-w::int)" - -fun - mult_raw :: "(nat \ nat) \ (nat \ nat) \ (nat \ nat)" -where - "mult_raw (x, y) (u, v) = (x*u + y*v, x*v + y*u)" - -quotient_def - mult_qnt::"int \ int \ int" -where - "mult_qnt \ mult_raw" - -definition - mult_int_def [code del]: "z * w = mult_qnt z w" - -fun - le_raw :: "(nat \ nat) \ (nat \ nat) \ bool" -where - "le_raw (x, y) (u, v) = (x+v \ u+y)" - -quotient_def - le_qnt :: "int \ int \ bool" -where - "le_qnt \ le_raw" - -definition - le_int_def [code del]: - "z \ w = le_qnt z w" - -definition - less_int_def [code del]: "(z\int) < w = (z \ w \ z \ w)" - -definition - zabs_def: "\i\int\ = (if i < 0 then - i else i)" - -definition - zsgn_def: "sgn (i\int) = (if i=0 then 0 else if 0 ===> op \ ===> op \) plus_raw plus_raw" -by auto - -lemma minus_raw_rsp[quotient_rsp]: - shows "(op \ ===> op \) minus_raw minus_raw" - by auto - -lemma mult_raw_rsp[quotient_rsp]: - shows "(op \ ===> op \ ===> op \) mult_raw mult_raw" -apply(auto) -apply(simp add: mult algebra_simps) -sorry - -lemma le_raw_rsp[quotient_rsp]: - shows "(op \ ===> op \ ===> op =) le_raw le_raw" -by auto - -lemma plus_assoc_raw: - shows "plus_raw (plus_raw i j) k \ plus_raw i (plus_raw j k)" -by (cases i, cases j, cases k) (simp) - -lemma plus_sym_raw: - shows "plus_raw i j \ plus_raw j i" -by (cases i, cases j) (simp) - -lemma plus_zero_raw: - shows "plus_raw (0, 0) i \ i" -by (cases i) (simp) - -lemma plus_minus_zero_raw: - shows "plus_raw (minus_raw i) i \ (0, 0)" -by (cases i) (simp) - -lemma mult_assoc_raw: - shows "mult_raw (mult_raw i j) k \ mult_raw i (mult_raw j k)" -by (cases i, cases j, cases k) - (simp add: mult algebra_simps) - -lemma mult_sym_raw: - shows "mult_raw i j \ mult_raw j i" -by (cases i, cases j) (simp) - -lemma mult_one_raw: - shows "mult_raw (1, 0) i \ i" -by (cases i) (simp) - -lemma mult_plus_comm_raw: - shows "mult_raw (plus_raw i j) k \ plus_raw (mult_raw i k) (mult_raw j k)" -by (cases i, cases j, cases k) - (simp add: mult algebra_simps) - -lemma one_zero_distinct: - shows "\ (0, 0) \ ((1::nat), (0::nat))" - by simp - -text{*The integers form a @{text comm_ring_1}*} - - -ML {* val qty = @{typ "int"} *} -ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} -ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "int" *} - -instance int :: comm_ring_1 -proof - fix i j k :: int - show "(i + j) + k = i + (j + k)" - unfolding add_int_def - apply(tactic {* lift_tac @{context} @{thm plus_assoc_raw} 1 *}) - done - show "i + j = j + i" - unfolding add_int_def - apply(tactic {* lift_tac @{context} @{thm plus_sym_raw} 1 *}) - done - show "0 + i = (i::int)" - unfolding add_int_def Zero_int_def - apply(tactic {* lift_tac @{context} @{thm plus_zero_raw} 1 *}) - done - show "- i + i = 0" - unfolding add_int_def minus_int_def Zero_int_def - apply(tactic {* lift_tac @{context} @{thm plus_minus_zero_raw} 1 *}) - done - show "i - j = i + - j" - by (simp add: diff_int_def) - show "(i * j) * k = i * (j * k)" - unfolding mult_int_def - apply(tactic {* lift_tac @{context} @{thm mult_assoc_raw} 1 *}) - done - show "i * j = j * i" - unfolding mult_int_def - apply(tactic {* lift_tac @{context} @{thm mult_sym_raw} 1 *}) - done - show "1 * i = i" - unfolding mult_int_def One_int_def - apply(tactic {* lift_tac @{context} @{thm mult_one_raw} 1 *}) - done - show "(i + j) * k = i * k + j * k" - unfolding mult_int_def add_int_def - apply(tactic {* lift_tac @{context} @{thm mult_plus_comm_raw} 1 *}) - done - show "0 \ (1::int)" - unfolding Zero_int_def One_int_def - apply(tactic {* lift_tac @{context} @{thm one_zero_distinct} 1 *}) - done -qed - -term of_nat -thm of_nat_def - -lemma int_def: "of_nat m = ABS_int (m, 0)" -apply(induct m) -apply(simp add: Zero_int_def zero_qnt_def) -apply(simp) -apply(simp add: add_int_def One_int_def) -apply(simp add: plus_qnt_def one_qnt_def) -oops - -lemma le_antisym_raw: - shows "le_raw i j \ le_raw j i \ i \ j" -by (cases i, cases j) (simp) - -lemma le_refl_raw: - shows "le_raw i i" -by (cases i) (simp) - -lemma le_trans_raw: - shows "le_raw i j \ le_raw j k \ le_raw i k" -by (cases i, cases j, cases k) (simp) - -lemma le_cases_raw: - shows "le_raw i j \ le_raw j i" -by (cases i, cases j) - (simp add: linorder_linear) - -instance int :: linorder -proof - fix i j k :: int - show antisym: "i \ j \ j \ i \ i = j" - unfolding le_int_def - apply(tactic {* lift_tac @{context} @{thm le_antisym_raw} 1 *}) - done - show "(i < j) = (i \ j \ \ j \ i)" - by (auto simp add: less_int_def dest: antisym) - show "i \ i" - unfolding le_int_def - apply(tactic {* lift_tac @{context} @{thm le_refl_raw} 1 *}) - done - show "i \ j \ j \ k \ i \ k" - unfolding le_int_def - apply(tactic {* lift_tac @{context} @{thm le_trans_raw} 1 *}) - done - show "i \ j \ j \ i" - unfolding le_int_def - apply(tactic {* lift_tac @{context} @{thm le_cases_raw} 1 *}) - done -qed - -instantiation int :: distrib_lattice -begin - -definition - "(inf \ int \ int \ int) = min" - -definition - "(sup \ int \ int \ int) = max" - -instance - by intro_classes - (auto simp add: inf_int_def sup_int_def min_max.sup_inf_distrib1) - -end - -lemma le_plus_raw: - shows "le_raw i j \ le_raw (plus_raw k i) (plus_raw k j)" -by (cases i, cases j, cases k) (simp) - - -instance int :: pordered_cancel_ab_semigroup_add -proof - fix i j k :: int - show "i \ j \ k + i \ k + j" - unfolding le_int_def add_int_def - apply(tactic {* lift_tac @{context} @{thm le_plus_raw} 1 *}) - done -qed - -lemma test: - "\le_raw i j \ \i \ j; le_raw (0, 0) k \ \(0, 0) \ k\ - \ le_raw (mult_raw k i) (mult_raw k j) \ \mult_raw k i \ mult_raw k j" -apply(cases i, cases j, cases k) -apply(auto simp add: mult algebra_simps) -sorry - - -text{*The integers form an ordered integral domain*} -instance int :: ordered_idom -proof - fix i j k :: int - show "i < j \ 0 < k \ k * i < k * j" - unfolding mult_int_def le_int_def less_int_def Zero_int_def - apply(tactic {* lift_tac @{context} @{thm test} 1 *}) - done - show "\i\ = (if i < 0 then -i else i)" - by (simp only: zabs_def) - show "sgn (i\int) = (if i=0 then 0 else if 0 'a" -where - "of_int -*) - - -subsection {* Binary representation *} - -text {* - This formalization defines binary arithmetic in terms of the integers - rather than using a datatype. This avoids multiple representations (leading - zeroes, etc.) See @{text "ZF/Tools/twos-compl.ML"}, function @{text - int_of_binary}, for the numerical interpretation. - - The representation expects that @{text "(m mod 2)"} is 0 or 1, - even if m is negative; - For instance, @{text "-5 div 2 = -3"} and @{text "-5 mod 2 = 1"}; thus - @{text "-5 = (-3)*2 + 1"}. - - This two's complement binary representation derives from the paper - "An Efficient Representation of Arithmetic for Term Rewriting" by - Dave Cohen and Phil Watson, Rewriting Techniques and Applications, - Springer LNCS 488 (240-251), 1991. -*} - -subsubsection {* The constructors @{term Bit0}, @{term Bit1}, @{term Pls} and @{term Min} *} - -definition - Pls :: int where - [code del]: "Pls = 0" - -definition - Min :: int where - [code del]: "Min = - 1" - -definition - Bit0 :: "int \ int" where - [code del]: "Bit0 k = k + k" - -definition - Bit1 :: "int \ int" where - [code del]: "Bit1 k = 1 + k + k" - -class number = -- {* for numeric types: nat, int, real, \dots *} - fixes number_of :: "int \ 'a" - -use "~~/src/HOL/Tools/numeral.ML" - -syntax - "_Numeral" :: "num_const \ 'a" ("_") - -use "~~/src/HOL/Tools/numeral_syntax.ML" -(* -setup NumeralSyntax.setup - -abbreviation - "Numeral0 \ number_of Pls" - -abbreviation - "Numeral1 \ number_of (Bit1 Pls)" - -lemma Let_number_of [simp]: "Let (number_of v) f = f (number_of v)" - -- {* Unfold all @{text let}s involving constants *} - unfolding Let_def .. - -definition - succ :: "int \ int" where - [code del]: "succ k = k + 1" - -definition - pred :: "int \ int" where - [code del]: "pred k = k - 1" - -lemmas - max_number_of [simp] = max_def - [of "number_of u" "number_of v", standard, simp] -and - min_number_of [simp] = min_def - [of "number_of u" "number_of v", standard, simp] - -- {* unfolding @{text minx} and @{text max} on numerals *} - -lemmas numeral_simps = - succ_def pred_def Pls_def Min_def Bit0_def Bit1_def - -text {* Removal of leading zeroes *} - -lemma Bit0_Pls [simp, code_post]: - "Bit0 Pls = Pls" - unfolding numeral_simps by simp - -lemma Bit1_Min [simp, code_post]: - "Bit1 Min = Min" - unfolding numeral_simps by simp - -lemmas normalize_bin_simps = - Bit0_Pls Bit1_Min -*) \ No newline at end of file diff -r 6088fea1c8b1 -r 8a1c8dc72b5c IsaMakefile --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/IsaMakefile Mon Dec 07 14:09:50 2009 +0100 @@ -0,0 +1,31 @@ + +## targets + +default: Quot +images: +test: Quot + +all: images test + + +## global settings + +SRC = $(ISABELLE_HOME)/src +OUT = $(ISABELLE_OUTPUT) +LOG = $(OUT)/log + +USEDIR = $(ISABELLE_TOOL) usedir -v true -i true -d pdf ## -D generated + + +## Quot + +Quot: $(LOG)/HOL-Quot.gz + +$(LOG)/HOL-Quot.gz: Quot/ROOT.ML Quot/*.thy + @$(USEDIR) HOL Quot + + +## clean + +clean: + @rm -f $(LOG)/HOL-Quot.gz diff -r 6088fea1c8b1 -r 8a1c8dc72b5c LFex.thy --- a/LFex.thy Mon Dec 07 14:00:36 2009 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,307 +0,0 @@ -theory LFex -imports Nominal QuotMain -begin - -atom_decl name ident - -nominal_datatype kind = - Type - | KPi "ty" "name" "kind" -and ty = - TConst "ident" - | TApp "ty" "trm" - | TPi "ty" "name" "ty" -and trm = - Const "ident" - | Var "name" - | App "trm" "trm" - | Lam "ty" "name" "trm" - -function - fv_kind :: "kind \ name set" -and fv_ty :: "ty \ name set" -and fv_trm :: "trm \ name set" -where - "fv_kind (Type) = {}" -| "fv_kind (KPi A x K) = (fv_ty A) \ ((fv_kind K) - {x})" -| "fv_ty (TConst i) = {}" -| "fv_ty (TApp A M) = (fv_ty A) \ (fv_trm M)" -| "fv_ty (TPi A x B) = (fv_ty A) \ ((fv_ty B) - {x})" -| "fv_trm (Const i) = {}" -| "fv_trm (Var x) = {x}" -| "fv_trm (App M N) = (fv_trm M) \ (fv_trm N)" -| "fv_trm (Lam A x M) = (fv_ty A) \ ((fv_trm M) - {x})" -sorry - -termination fv_kind sorry - -inductive - akind :: "kind \ kind \ bool" ("_ \ki _" [100, 100] 100) -and aty :: "ty \ ty \ bool" ("_ \ty _" [100, 100] 100) -and atrm :: "trm \ trm \ bool" ("_ \tr _" [100, 100] 100) -where - a1: "(Type) \ki (Type)" -| a21: "\A \ty A'; K \ki K'\ \ (KPi A x K) \ki (KPi A' x K')" -| a22: "\A \ty A'; K \ki ([(x,x')]\K'); x \ (fv_ty A'); x \ ((fv_kind K') - {x'})\ - \ (KPi A x K) \ki (KPi A' x' K')" -| a3: "i = j \ (TConst i) \ty (TConst j)" -| a4: "\A \ty A'; M \tr M'\ \ (TApp A M) \ty (TApp A' M')" -| a51: "\A \ty A'; B \ty B'\ \ (TPi A x B) \ty (TPi A' x B')" -| a52: "\A \ty A'; B \ty ([(x,x')]\B'); x \ (fv_ty B'); x \ ((fv_ty B') - {x'})\ - \ (TPi A x B) \ty (TPi A' x' B')" -| a6: "i = j \ (Const i) \trm (Const j)" -| a7: "x = y \ (Var x) \trm (Var y)" -| a8: "\M \trm M'; N \tr N'\ \ (App M N) \tr (App M' N')" -| a91: "\A \ty A'; M \tr M'\ \ (Lam A x M) \tr (Lam A' x M')" -| a92: "\A \ty A'; M \tr ([(x,x')]\M'); x \ (fv_ty B'); x \ ((fv_trm M') - {x'})\ - \ (Lam A x M) \tr (Lam A' x' M')" - -lemma al_refl: - fixes K::"kind" - and A::"ty" - and M::"trm" - shows "K \ki K" - and "A \ty A" - and "M \tr M" - apply(induct K and A and M rule: kind_ty_trm.inducts) - apply(auto intro: akind_aty_atrm.intros) - done - -lemma alpha_equivps: - shows "equivp akind" - and "equivp aty" - and "equivp atrm" -sorry - -quotient KIND = kind / akind - by (rule alpha_equivps) - -quotient TY = ty / aty - and TRM = trm / atrm - by (auto intro: alpha_equivps) - -print_quotients - -quotient_def - TYP :: "KIND" -where - "TYP \ Type" - -quotient_def - KPI :: "TY \ name \ KIND \ KIND" -where - "KPI \ KPi" - -quotient_def - TCONST :: "ident \ TY" -where - "TCONST \ TConst" - -quotient_def - TAPP :: "TY \ TRM \ TY" -where - "TAPP \ TApp" - -quotient_def - TPI :: "TY \ name \ TY \ TY" -where - "TPI \ TPi" - -(* FIXME: does not work with CONST *) -quotient_def - CONS :: "ident \ TRM" -where - "CONS \ Const" - -quotient_def - VAR :: "name \ TRM" -where - "VAR \ Var" - -quotient_def - APP :: "TRM \ TRM \ TRM" -where - "APP \ App" - -quotient_def - LAM :: "TY \ name \ TRM \ TRM" -where - "LAM \ Lam" - -thm TYP_def -thm KPI_def -thm TCONST_def -thm TAPP_def -thm TPI_def -thm VAR_def -thm CONS_def -thm APP_def -thm LAM_def - -(* FIXME: print out a warning if the type contains a liftet type, like kind \ name set *) -quotient_def - FV_kind :: "KIND \ name set" -where - "FV_kind \ fv_kind" - -quotient_def - FV_ty :: "TY \ name set" -where - "FV_ty \ fv_ty" - -quotient_def - FV_trm :: "TRM \ name set" -where - "FV_trm \ fv_trm" - -thm FV_kind_def -thm FV_ty_def -thm FV_trm_def - -(* FIXME: does not work yet *) -overloading - perm_kind \ "perm :: 'x prm \ KIND \ KIND" (unchecked) - perm_ty \ "perm :: 'x prm \ TY \ TY" (unchecked) - perm_trm \ "perm :: 'x prm \ TRM \ TRM" (unchecked) -begin - -quotient_def - perm_kind :: "'x prm \ KIND \ KIND" -where - "perm_kind \ (perm::'x prm \ kind \ kind)" - -quotient_def - perm_ty :: "'x prm \ TY \ TY" -where - "perm_ty \ (perm::'x prm \ ty \ ty)" - -quotient_def - perm_trm :: "'x prm \ TRM \ TRM" -where - "perm_trm \ (perm::'x prm \ trm \ trm)" - -(* TODO/FIXME: Think whether these RSP theorems are true. *) -lemma kpi_rsp[quotient_rsp]: - "(aty ===> op = ===> akind ===> akind) KPi KPi" sorry -lemma tconst_rsp[quotient_rsp]: - "(op = ===> aty) TConst TConst" sorry -lemma tapp_rsp[quotient_rsp]: - "(aty ===> atrm ===> aty) TApp TApp" sorry -lemma tpi_rsp[quotient_rsp]: - "(aty ===> op = ===> aty ===> aty) TPi TPi" sorry -lemma var_rsp[quotient_rsp]: - "(op = ===> atrm) Var Var" sorry -lemma app_rsp[quotient_rsp]: - "(atrm ===> atrm ===> atrm) App App" sorry -lemma const_rsp[quotient_rsp]: - "(op = ===> atrm) Const Const" sorry -lemma lam_rsp[quotient_rsp]: - "(aty ===> op = ===> atrm ===> atrm) Lam Lam" sorry - -lemma perm_kind_rsp[quotient_rsp]: - "(op = ===> akind ===> akind) op \ op \" sorry -lemma perm_ty_rsp[quotient_rsp]: - "(op = ===> aty ===> aty) op \ op \" sorry -lemma perm_trm_rsp[quotient_rsp]: - "(op = ===> atrm ===> atrm) op \ op \" sorry - -lemma fv_ty_rsp[quotient_rsp]: - "(aty ===> op =) fv_ty fv_ty" sorry -lemma fv_kind_rsp[quotient_rsp]: - "(akind ===> op =) fv_kind fv_kind" sorry -lemma fv_trm_rsp[quotient_rsp]: - "(atrm ===> op =) fv_trm fv_trm" sorry - - -thm akind_aty_atrm.induct -thm kind_ty_trm.induct - -ML {* - val quot = @{thms Quotient_KIND Quotient_TY Quotient_TRM} - val rel_refl = map (fn x => @{thm equivp_reflp} OF [x]) @{thms alpha_equivps} - val reps_same = map (fn x => @{thm Quotient_rel_rep} OF [x]) quot - val trans2 = map (fn x => @{thm equals_rsp} OF [x]) quot -*} - -lemma - assumes a0: - "P1 TYP TYP" - and a1: - "\A A' K K' x. \(A::TY) = A'; P2 A A'; (K::KIND) = K'; P1 K K'\ - \ P1 (KPI A x K) (KPI A' x K')" - and a2: - "\A A' K K' x x'. \(A ::TY) = A'; P2 A A'; (K :: KIND) = ([(x, x')] \ K'); P1 K ([(x, x')] \ K'); - x \ FV_ty A'; x \ FV_kind K' - {x'}\ \ P1 (KPI A x K) (KPI A' x' K')" - and a3: - "\i j. i = j \ P2 (TCONST i) (TCONST j)" - and a4: - "\A A' M M'. \(A ::TY) = A'; P2 A A'; (M :: TRM) = M'; P3 M M'\ \ P2 (TAPP A M) (TAPP A' M')" - and a5: - "\A A' B B' x. \(A ::TY) = A'; P2 A A'; (B ::TY) = B'; P2 B B'\ \ P2 (TPI A x B) (TPI A' x B')" - and a6: - "\A A' B x x' B'. \(A ::TY) = A'; P2 A A'; (B ::TY) = ([(x, x')] \ B'); P2 B ([(x, x')] \ B'); - x \ FV_ty B'; x \ FV_ty B' - {x'}\ \ P2 (TPI A x B) (TPI A' x' B')" - and a7: - "\i j m. i = j \ P3 (CONS i) (m (CONS j))" - and a8: - "\x y m. x = y \ P3 (VAR x) (m (VAR y))" - and a9: - "\M m M' N N'. \(M :: TRM) = m M'; P3 M (m M'); (N :: TRM) = N'; P3 N N'\ \ P3 (APP M N) (APP M' N')" - and a10: - "\A A' M M' x. \(A ::TY) = A'; P2 A A'; (M :: TRM) = M'; P3 M M'\ \ P3 (LAM A x M) (LAM A' x M')" - and a11: - "\A A' M x x' M' B'. \(A ::TY) = A'; P2 A A'; (M :: TRM) = ([(x, x')] \ M'); P3 M ([(x, x')] \ M'); - x \ FV_ty B'; x \ FV_trm M' - {x'}\ \ P3 (LAM A x M) (LAM A' x' M')" - shows "((x1 :: KIND) = x2 \ P1 x1 x2) \ - ((x3 ::TY) = x4 \ P2 x3 x4) \ - ((x5 :: TRM) = x6 \ P3 x5 x6)" -using a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 -apply - -apply(tactic {* procedure_tac @{context} @{thm akind_aty_atrm.induct} 1 *}) -apply(tactic {* regularize_tac @{context} 1 *}) -apply(tactic {* all_inj_repabs_tac @{context} rel_refl trans2 1 *}) -apply(fold perm_kind_def perm_ty_def perm_trm_def) -apply(tactic {* clean_tac @{context} 1 *}) -(* -Profiling: -ML_prf {* fun ith i = (#concl (fst (Subgoal.focus @{context} i (#goal (Isar.goal ()))))) *} -ML_prf {* profile 2 Seq.list_of ((clean_tac @{context} quot defs 1) (ith 3)) *} -ML_prf {* profile 2 Seq.list_of ((regularize_tac @{context} @{thms alpha_equivps} 1) (ith 1)) *} -ML_prf {* PolyML.profiling 1 *} -ML_prf {* profile 2 Seq.list_of ((all_inj_repabs_tac @{context} quot rel_refl trans2 1) (#goal (Isar.goal ()))) *} -*) -done - -(* Does not work: -lemma - assumes a0: "P1 TYP" - and a1: "\ty name kind. \P2 ty; P1 kind\ \ P1 (KPI ty name kind)" - and a2: "\id. P2 (TCONST id)" - and a3: "\ty trm. \P2 ty; P3 trm\ \ P2 (TAPP ty trm)" - and a4: "\ty1 name ty2. \P2 ty1; P2 ty2\ \ P2 (TPI ty1 name ty2)" - and a5: "\id. P3 (CONS id)" - and a6: "\name. P3 (VAR name)" - and a7: "\trm1 trm2. \P3 trm1; P3 trm2\ \ P3 (APP trm1 trm2)" - and a8: "\ty name trm. \P2 ty; P3 trm\ \ P3 (LAM ty name trm)" - shows "P1 mkind \ P2 mty \ P3 mtrm" -using a0 a1 a2 a3 a4 a5 a6 a7 a8 -*) - -lemma "\P TYP; - \ty name kind. \Q ty; P kind\ \ P (KPI ty name kind); - \id. Q (TCONST id); - \ty trm. \Q ty; R trm\ \ Q (TAPP ty trm); - \ty1 name ty2. \Q ty1; Q ty2\ \ Q (TPI ty1 name ty2); - \id. R (CONS id); \name. R (VAR name); - \trm1 trm2. \R trm1; R trm2\ \ R (APP trm1 trm2); - \ty name trm. \Q ty; R trm\ \ R (LAM ty name trm)\ - \ P mkind \ Q mty \ R mtrm" -apply(tactic {* lift_tac @{context} @{thm kind_ty_trm.induct} 1 *}) -done - -print_quotients - -end - - - diff -r 6088fea1c8b1 -r 8a1c8dc72b5c LamEx.thy --- a/LamEx.thy Mon Dec 07 14:00:36 2009 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,252 +0,0 @@ -theory LamEx -imports Nominal QuotMain -begin - -atom_decl name - -thm abs_fresh(1) - -nominal_datatype rlam = - rVar "name" -| rApp "rlam" "rlam" -| rLam "name" "rlam" - -print_theorems - -function - rfv :: "rlam \ name set" -where - rfv_var: "rfv (rVar a) = {a}" -| rfv_app: "rfv (rApp t1 t2) = (rfv t1) \ (rfv t2)" -| rfv_lam: "rfv (rLam a t) = (rfv t) - {a}" -sorry - -termination rfv sorry - -inductive - alpha :: "rlam \ rlam \ bool" ("_ \ _" [100, 100] 100) -where - a1: "a = b \ (rVar a) \ (rVar b)" -| a2: "\t1 \ t2; s1 \ s2\ \ rApp t1 s1 \ rApp t2 s2" -| a3: "\t \ ([(a,b)]\s); a \ rfv (rLam b t)\ \ rLam a t \ rLam b s" - -print_theorems - -lemma alpha_refl: - fixes t::"rlam" - shows "t \ t" - apply(induct t rule: rlam.induct) - apply(simp add: a1) - apply(simp add: a2) - apply(rule a3) - apply(subst pt_swap_bij'') - apply(rule pt_name_inst) - apply(rule at_name_inst) - apply(simp) - apply(simp) - done - -lemma alpha_equivp: - shows "equivp alpha" -sorry - -quotient lam = rlam / alpha - apply(rule alpha_equivp) - done - -print_quotients - -quotient_def - Var :: "name \ lam" -where - "Var \ rVar" - -quotient_def - App :: "lam \ lam \ lam" -where - "App \ rApp" - -quotient_def - Lam :: "name \ lam \ lam" -where - "Lam \ rLam" - -thm Var_def -thm App_def -thm Lam_def - -quotient_def - fv :: "lam \ name set" -where - "fv \ rfv" - -thm fv_def - -(* definition of overloaded permutation function *) -(* for the lifted type lam *) -overloading - perm_lam \ "perm :: 'x prm \ lam \ lam" (unchecked) -begin - -quotient_def - perm_lam :: "'x prm \ lam \ lam" -where - "perm_lam \ (perm::'x prm \ rlam \ rlam)" - -end - -(*quotient_def (for lam) - abs_fun_lam :: "'x prm \ lam \ lam" -where - "perm_lam \ (perm::'x prm \ rlam \ rlam)"*) - - -thm perm_lam_def - -(* lemmas that need to lift *) -lemma pi_var_com: - fixes pi::"'x prm" - shows "(pi\rVar a) \ rVar (pi\a)" - sorry - -lemma pi_app_com: - fixes pi::"'x prm" - shows "(pi\rApp t1 t2) \ rApp (pi\t1) (pi\t2)" - sorry - -lemma pi_lam_com: - fixes pi::"'x prm" - shows "(pi\rLam a t) \ rLam (pi\a) (pi\t)" - sorry - - - -lemma real_alpha: - assumes a: "t = [(a,b)]\s" "a\[b].s" - shows "Lam a t = Lam b s" -using a -unfolding fresh_def supp_def -sorry - -lemma perm_rsp[quotient_rsp]: - "(op = ===> alpha ===> alpha) op \ op \" - apply(auto) - (* this is propably true if some type conditions are imposed ;o) *) - sorry - -lemma fresh_rsp: - "(op = ===> alpha ===> op =) fresh fresh" - apply(auto) - (* this is probably only true if some type conditions are imposed *) - sorry - -lemma rVar_rsp[quotient_rsp]: - "(op = ===> alpha) rVar rVar" -by (auto intro:a1) - -lemma rApp_rsp[quotient_rsp]: "(alpha ===> alpha ===> alpha) rApp rApp" -by (auto intro:a2) - -lemma rLam_rsp[quotient_rsp]: "(op = ===> alpha ===> alpha) rLam rLam" - apply(auto) - apply(rule a3) - apply(rule_tac t="[(x,x)]\y" and s="y" in subst) - apply(rule sym) - apply(rule trans) - apply(rule pt_name3) - apply(rule at_ds1[OF at_name_inst]) - apply(simp add: pt_name1) - apply(assumption) - apply(simp add: abs_fresh) - done - -lemma rfv_rsp[quotient_rsp]: "(alpha ===> op =) rfv rfv" - sorry - -lemma rvar_inject: "rVar a \ rVar b = (a = b)" -apply (auto) -apply (erule alpha.cases) -apply (simp_all add: rlam.inject alpha_refl) -done - -ML {* val qty = @{typ "lam"} *} -ML {* val rsp_thms = @{thms perm_rsp fresh_rsp rVar_rsp rApp_rsp rLam_rsp rfv_rsp} *} - -ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} -ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "lam" *} -ML {* fun lift_tac_lam lthy t = lift_tac lthy t *} - -lemma pi_var: "(pi\('x \ 'x) list) \ Var a = Var (pi \ a)" -apply (tactic {* lift_tac_lam @{context} @{thm pi_var_com} 1 *}) -done - -lemma pi_app: "(pi\('x \ 'x) list) \ App (x\lam) (xa\lam) = App (pi \ x) (pi \ xa)" -apply (tactic {* lift_tac_lam @{context} @{thm pi_app_com} 1 *}) -done - -lemma pi_lam: "(pi\('x \ 'x) list) \ Lam (a\name) (x\lam) = Lam (pi \ a) (pi \ x)" -apply (tactic {* lift_tac_lam @{context} @{thm pi_lam_com} 1 *}) -done - -lemma fv_var: "fv (Var (a\name)) = {a}" -apply (tactic {* lift_tac_lam @{context} @{thm rfv_var} 1 *}) -done - -lemma fv_app: "fv (App (x\lam) (xa\lam)) = fv x \ fv xa" -apply (tactic {* lift_tac_lam @{context} @{thm rfv_app} 1 *}) -done - -lemma fv_lam: "fv (Lam (a\name) (x\lam)) = fv x - {a}" -apply (tactic {* lift_tac_lam @{context} @{thm rfv_lam} 1 *}) -done - -lemma a1: "(a\name) = (b\name) \ Var a = Var b" -apply (tactic {* lift_tac_lam @{context} @{thm a1} 1 *}) -done - -lemma a2: "\(x\lam) = (xa\lam); (xb\lam) = (xc\lam)\ \ App x xb = App xa xc" -apply (tactic {* lift_tac_lam @{context} @{thm a2} 1 *}) -done - -lemma a3: "\(x\lam) = [(a\name, b\name)] \ (xa\lam); a \ fv (Lam b x)\ \ Lam a x = Lam b xa" -apply (tactic {* lift_tac_lam @{context} @{thm a3} 1 *}) -done - -lemma alpha_cases: "\a1 = a2; \a b. \a1 = Var a; a2 = Var b; a = b\ \ P; - \x xa xb xc. \a1 = App x xb; a2 = App xa xc; x = xa; xb = xc\ \ P; - \x a b xa. \a1 = Lam a x; a2 = Lam b xa; x = [(a, b)] \ xa; a \ fv (Lam b x)\ \ P\ - \ P" -apply (tactic {* lift_tac_lam @{context} @{thm alpha.cases} 1 *}) -done - -lemma alpha_induct: "\(qx\lam) = (qxa\lam); \(a\name) b\name. a = b \ (qxb\lam \ lam \ bool) (Var a) (Var b); - \(x\lam) (xa\lam) (xb\lam) xc\lam. \x = xa; qxb x xa; xb = xc; qxb xb xc\ \ qxb (App x xb) (App xa xc); - \(x\lam) (a\name) (b\name) xa\lam. - \x = [(a, b)] \ xa; qxb x ([(a, b)] \ xa); a \ fv (Lam b x)\ \ qxb (Lam a x) (Lam b xa)\ - \ qxb qx qxa" -apply (tactic {* lift_tac_lam @{context} @{thm alpha.induct} 1 *}) -done - -lemma var_inject: "(Var a = Var b) = (a = b)" -apply (tactic {* lift_tac_lam @{context} @{thm rvar_inject} 1 *}) -done - -lemma lam_induct:" \\name. P (Var name); \lam1 lam2. \P lam1; P lam2\ \ P (App lam1 lam2); - \name lam. P lam \ P (Lam name lam)\ \ P lam" -apply (tactic {* lift_tac_lam @{context} @{thm rlam.induct} 1 *}) -done - -lemma var_supp: - shows "supp (Var a) = ((supp a)::name set)" - apply(simp add: supp_def) - apply(simp add: pi_var) - apply(simp add: var_inject) - done - -lemma var_fresh: - fixes a::"name" - shows "(a\(Var b)) = (a\b)" - apply(simp add: fresh_def) - apply(simp add: var_supp) - done - diff -r 6088fea1c8b1 -r 8a1c8dc72b5c Prove.thy --- a/Prove.thy Mon Dec 07 14:00:36 2009 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,28 +0,0 @@ -theory Prove -imports Plain -begin - -ML {* -val r = Unsynchronized.ref (NONE:(unit -> term) option) -*} - -ML {* -let - fun after_qed thm_name thms lthy = - Local_Theory.note (thm_name, (flat thms)) lthy |> snd - - fun setup_proof (name_spec, (txt, pos)) lthy = - let - val trm = ML_Context.evaluate lthy true ("r", r) txt - in - Proof.theorem_i NONE (after_qed name_spec) [[(trm,[])]] lthy - end - - val parser = SpecParse.opt_thm_name ":" -- OuterParse.ML_source -in - OuterSyntax.local_theory_to_proof "prove" "proving a proposition" - OuterKeyword.thy_goal (parser >> setup_proof) -end -*} - -end diff -r 6088fea1c8b1 -r 8a1c8dc72b5c Quot/Examples/FSet.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Quot/Examples/FSet.thy Mon Dec 07 14:09:50 2009 +0100 @@ -0,0 +1,440 @@ +theory FSet +imports "../QuotMain" +begin + +inductive + list_eq (infix "\" 50) +where + "a#b#xs \ b#a#xs" +| "[] \ []" +| "xs \ ys \ ys \ xs" +| "a#a#xs \ a#xs" +| "xs \ ys \ a#xs \ a#ys" +| "\xs1 \ xs2; xs2 \ xs3\ \ xs1 \ xs3" + +lemma list_eq_refl: + shows "xs \ xs" + by (induct xs) (auto intro: list_eq.intros) + +lemma equivp_list_eq: + shows "equivp list_eq" + unfolding equivp_reflp_symp_transp reflp_def symp_def transp_def + apply(auto intro: list_eq.intros list_eq_refl) + done + +quotient fset = "'a list" / "list_eq" + apply(rule equivp_list_eq) + done + +print_theorems + +typ "'a fset" +thm "Rep_fset" +thm "ABS_fset_def" + +quotient_def + EMPTY :: "'a fset" +where + "EMPTY \ ([]::'a list)" + +term Nil +term EMPTY +thm EMPTY_def + +quotient_def + INSERT :: "'a \ 'a fset \ 'a fset" +where + "INSERT \ op #" + +term Cons +term INSERT +thm INSERT_def + +quotient_def + FUNION :: "'a fset \ 'a fset \ 'a fset" +where + "FUNION \ (op @)" + +term append +term FUNION +thm FUNION_def + +thm Quotient_fset + +thm QUOT_TYPE_I_fset.thm11 + + +fun + membship :: "'a \ 'a list \ bool" (infix "memb" 100) +where + m1: "(x memb []) = False" +| m2: "(x memb (y#xs)) = ((x=y) \ (x memb xs))" + +fun + card1 :: "'a list \ nat" +where + card1_nil: "(card1 []) = 0" +| card1_cons: "(card1 (x # xs)) = (if (x memb xs) then (card1 xs) else (Suc (card1 xs)))" + +quotient_def + CARD :: "'a fset \ nat" +where + "CARD \ card1" + +term card1 +term CARD +thm CARD_def + +(* text {* + Maybe make_const_def should require a theorem that says that the particular lifted function + respects the relation. With it such a definition would be impossible: + make_const_def @{binding CARD} @{term "length"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd +*}*) + +lemma card1_0: + fixes a :: "'a list" + shows "(card1 a = 0) = (a = [])" + by (induct a) auto + +lemma not_mem_card1: + fixes x :: "'a" + fixes xs :: "'a list" + shows "(~(x memb xs)) = (card1 (x # xs) = Suc (card1 xs))" + by auto + +lemma mem_cons: + fixes x :: "'a" + fixes xs :: "'a list" + assumes a : "x memb xs" + shows "x # xs \ xs" + using a by (induct xs) (auto intro: list_eq.intros ) + +lemma card1_suc: + fixes xs :: "'a list" + fixes n :: "nat" + assumes c: "card1 xs = Suc n" + shows "\a ys. ~(a memb ys) \ xs \ (a # ys)" + using c +apply(induct xs) +apply (metis Suc_neq_Zero card1_0) +apply (metis QUOT_TYPE_I_fset.R_trans card1_cons list_eq_refl mem_cons) +done + +definition + rsp_fold +where + "rsp_fold f = ((!u v. (f u v = f v u)) \ (!u v w. ((f u (f v w) = f (f u v) w))))" + +primrec + fold1 +where + "fold1 f (g :: 'a \ 'b) (z :: 'b) [] = z" +| "fold1 f g z (a # A) = + (if rsp_fold f + then ( + if (a memb A) then (fold1 f g z A) else (f (g a) (fold1 f g z A)) + ) else z)" + +lemma fs1_strong_cases: + fixes X :: "'a list" + shows "(X = []) \ (\a. \ Y. (~(a memb Y) \ (X \ a # Y)))" + apply (induct X) + apply (simp) + apply (metis QUOT_TYPE_I_fset.thm11 list_eq_refl mem_cons m1) + done + +quotient_def + IN :: "'a \ 'a fset \ bool" +where + "IN \ membship" + +term membship +term IN +thm IN_def + +term fold1 +quotient_def + FOLD :: "('a \ 'a \ 'a) \ ('b \ 'a) \ 'a \ 'b fset \ 'a" +where + "FOLD \ fold1" + +term fold1 +term fold +thm fold_def + +quotient_def + fmap::"('a \ 'b) \ 'a fset \ 'b fset" +where + "fmap \ map" + +term map +term fmap +thm fmap_def + +lemma memb_rsp: + fixes z + assumes a: "x \ y" + shows "(z memb x) = (z memb y)" + using a by induct auto + +lemma ho_memb_rsp[quotient_rsp]: + "(op = ===> (op \ ===> op =)) (op memb) (op memb)" + by (simp add: memb_rsp) + +lemma card1_rsp: + fixes a b :: "'a list" + assumes e: "a \ b" + shows "card1 a = card1 b" + using e by induct (simp_all add:memb_rsp) + +lemma ho_card1_rsp[quotient_rsp]: + "(op \ ===> op =) card1 card1" + by (simp add: card1_rsp) + +lemma cons_rsp[quotient_rsp]: + fixes z + assumes a: "xs \ ys" + shows "(z # xs) \ (z # ys)" + using a by (rule list_eq.intros(5)) + +lemma ho_cons_rsp[quotient_rsp]: + "(op = ===> op \ ===> op \) op # op #" + by (simp add: cons_rsp) + +lemma append_rsp_fst: + assumes a : "l1 \ l2" + shows "(l1 @ s) \ (l2 @ s)" + using a + by (induct) (auto intro: list_eq.intros list_eq_refl) + +lemma append_end: + shows "(e # l) \ (l @ [e])" + apply (induct l) + apply (auto intro: list_eq.intros list_eq_refl) + done + +lemma rev_rsp: + shows "a \ rev a" + apply (induct a) + apply simp + apply (rule list_eq_refl) + apply simp_all + apply (rule list_eq.intros(6)) + prefer 2 + apply (rule append_rsp_fst) + apply assumption + apply (rule append_end) + done + +lemma append_sym_rsp: + shows "(a @ b) \ (b @ a)" + apply (rule list_eq.intros(6)) + apply (rule append_rsp_fst) + apply (rule rev_rsp) + apply (rule list_eq.intros(6)) + apply (rule rev_rsp) + apply (simp) + apply (rule append_rsp_fst) + apply (rule list_eq.intros(3)) + apply (rule rev_rsp) + done + +lemma append_rsp: + assumes a : "l1 \ r1" + assumes b : "l2 \ r2 " + shows "(l1 @ l2) \ (r1 @ r2)" + apply (rule list_eq.intros(6)) + apply (rule append_rsp_fst) + using a apply (assumption) + apply (rule list_eq.intros(6)) + apply (rule append_sym_rsp) + apply (rule list_eq.intros(6)) + apply (rule append_rsp_fst) + using b apply (assumption) + apply (rule append_sym_rsp) + done + +lemma ho_append_rsp[quotient_rsp]: + "(op \ ===> op \ ===> op \) op @ op @" + by (simp add: append_rsp) + +lemma map_rsp: + assumes a: "a \ b" + shows "map f a \ map f b" + using a + apply (induct) + apply(auto intro: list_eq.intros) + done + +lemma ho_map_rsp[quotient_rsp]: + "(op = ===> op \ ===> op \) map map" + by (simp add: map_rsp) + +lemma map_append: + "(map f (a @ b)) \ (map f a) @ (map f b)" + by simp (rule list_eq_refl) + +lemma ho_fold_rsp[quotient_rsp]: + "(op = ===> op = ===> op = ===> op \ ===> op =) fold1 fold1" + apply (auto) + apply (case_tac "rsp_fold x") + prefer 2 + apply (erule_tac list_eq.induct) + apply (simp_all) + apply (erule_tac list_eq.induct) + apply (simp_all) + apply (auto simp add: memb_rsp rsp_fold_def) +done + +lemma list_equiv_rsp[quotient_rsp]: + shows "(op \ ===> op \ ===> op =) op \ op \" +by (auto intro: list_eq.intros) + +print_quotients + +ML {* val qty = @{typ "'a fset"} *} +ML {* val rsp_thms = + @{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp ho_map_rsp ho_append_rsp ho_fold_rsp} *} + +ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} +ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "fset"; *} +ML {* fun lift_tac_fset lthy t = lift_tac lthy t *} + +lemma "IN x EMPTY = False" +apply(tactic {* procedure_tac @{context} @{thm m1} 1 *}) +apply(tactic {* regularize_tac @{context} 1 *}) +apply(tactic {* all_inj_repabs_tac @{context} [rel_refl] [trans2] 1 *}) +apply(tactic {* clean_tac @{context} 1*}) +done + +lemma "IN x (INSERT y xa) = (x = y \ IN x xa)" +by (tactic {* lift_tac_fset @{context} @{thm m2} 1 *}) + +lemma "INSERT a (INSERT a x) = INSERT a x" +apply (tactic {* lift_tac_fset @{context} @{thm list_eq.intros(4)} 1 *}) +done + +lemma "x = xa \ INSERT a x = INSERT a xa" +apply (tactic {* lift_tac_fset @{context} @{thm list_eq.intros(5)} 1 *}) +done + +lemma "CARD x = Suc n \ (\a b. \ IN a b & x = INSERT a b)" +apply (tactic {* lift_tac_fset @{context} @{thm card1_suc} 1 *}) +done + +lemma "(\ IN x xa) = (CARD (INSERT x xa) = Suc (CARD xa))" +apply (tactic {* lift_tac_fset @{context} @{thm not_mem_card1} 1 *}) +done + +lemma "FOLD f g (z::'b) (INSERT a x) = + (if rsp_fold f then if IN a x then FOLD f g z x else f (g a) (FOLD f g z x) else z)" +apply(tactic {* lift_tac_fset @{context} @{thm fold1.simps(2)} 1 *}) +done + +ML {* fun inj_repabs_tac_fset lthy = inj_repabs_tac lthy [rel_refl] [trans2] *} + +lemma "fmap f (FUNION (x::'b fset) (xa::'b fset)) = FUNION (fmap f x) (fmap f xa)" +apply (tactic {* lift_tac_fset @{context} @{thm map_append} 1 *}) +done + +lemma "FUNION (FUNION x xa) xb = FUNION x (FUNION xa xb)" +apply (tactic {* lift_tac_fset @{context} @{thm append_assoc} 1 *}) +done + + +lemma "\P EMPTY; \a x. P x \ P (INSERT a x)\ \ P l" +apply (tactic {* (ObjectLogic.full_atomize_tac THEN' gen_frees_tac @{context}) 1 *}) +apply(tactic {* procedure_tac @{context} @{thm list.induct} 1 *}) +apply(tactic {* regularize_tac @{context} 1 *}) +defer +apply(tactic {* clean_tac @{context} 1 *}) +apply(tactic {* inj_repabs_tac_fset @{context} 1*})+ +done + +lemma list_induct_part: + assumes a: "P (x :: 'a list) ([] :: 'c list)" + assumes b: "\e t. P x t \ P x (e # t)" + shows "P x l" + apply (rule_tac P="P x" in list.induct) + apply (rule a) + apply (rule b) + apply (assumption) + done + +ML {* quot *} +thm quotient_thm + +lemma "P (x :: 'a list) (EMPTY :: 'c fset) \ (\e t. P x t \ P x (INSERT e t)) \ P x l" +apply (tactic {* lift_tac_fset @{context} @{thm list_induct_part} 1 *}) +done + +lemma "P (x :: 'a fset) (EMPTY :: 'c fset) \ (\e t. P x t \ P x (INSERT e t)) \ P x l" +apply (tactic {* lift_tac_fset @{context} @{thm list_induct_part} 1 *}) +done + +lemma "P (x :: 'a fset) ([] :: 'c list) \ (\e t. P x t \ P x (e # t)) \ P x l" +apply (tactic {* lift_tac_fset @{context} @{thm list_induct_part} 1 *}) +done + +quotient fset2 = "'a list" / "list_eq" + apply(rule equivp_list_eq) + done + +quotient_def + EMPTY2 :: "'a fset2" +where + "EMPTY2 \ ([]::'a list)" + +quotient_def + INSERT2 :: "'a \ 'a fset2 \ 'a fset2" +where + "INSERT2 \ op #" + +ML {* val quot = @{thms Quotient_fset Quotient_fset2} *} +ML {* fun inj_repabs_tac_fset lthy = inj_repabs_tac lthy [rel_refl] [trans2] *} +ML {* fun lift_tac_fset lthy t = lift_tac lthy t *} + +lemma "P (x :: 'a fset2) (EMPTY :: 'c fset) \ (\e t. P x t \ P x (INSERT e t)) \ P x l" +apply (tactic {* lift_tac_fset @{context} @{thm list_induct_part} 1 *}) +done + +lemma "P (x :: 'a fset) (EMPTY2 :: 'c fset2) \ (\e t. P x t \ P x (INSERT2 e t)) \ P x l" +apply (tactic {* lift_tac_fset @{context} @{thm list_induct_part} 1 *}) +done + +quotient_def + fset_rec::"'a \ ('b \ 'b fset \ 'a \ 'a) \ 'b fset \ 'a" +where + "fset_rec \ list_rec" + +quotient_def + fset_case::"'a \ ('b \ 'b fset \ 'a) \ 'b fset \ 'a" +where + "fset_case \ list_case" + +(* Probably not true without additional assumptions about the function *) +lemma list_rec_rsp[quotient_rsp]: + "(op = ===> (op = ===> op \ ===> op =) ===> op \ ===> op =) list_rec list_rec" + apply (auto) + apply (erule_tac list_eq.induct) + apply (simp_all) + sorry + +lemma list_case_rsp[quotient_rsp]: + "(op = ===> (op = ===> op \ ===> op =) ===> op \ ===> op =) list_case list_case" + apply (auto) + sorry + +ML {* val rsp_thms = @{thms list_rec_rsp list_case_rsp} @ rsp_thms *} +ML {* fun lift_tac_fset lthy t = lift_tac lthy t *} + +lemma "fset_rec (f1::'t) x (INSERT a xa) = x a xa (fset_rec f1 x xa)" +apply (tactic {* lift_tac_fset @{context} @{thm list.recs(2)} 1 *}) +done + +lemma "fset_case (f1::'t) f2 (INSERT a xa) = f2 a xa" +apply (tactic {* lift_tac_fset @{context} @{thm list.cases(2)} 1 *}) +done + + +end diff -r 6088fea1c8b1 -r 8a1c8dc72b5c Quot/Examples/IntEx.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Quot/Examples/IntEx.thy Mon Dec 07 14:09:50 2009 +0100 @@ -0,0 +1,276 @@ +theory IntEx +imports "../QuotMain" +begin + +fun + intrel :: "(nat \ nat) \ (nat \ nat) \ bool" (infix "\" 50) +where + "intrel (x, y) (u, v) = (x + v = u + y)" + +quotient my_int = "nat \ nat" / intrel + apply(unfold equivp_def) + apply(auto simp add: mem_def expand_fun_eq) + done + +thm quotient_equiv + +thm quotient_thm + +thm my_int_equivp + +print_theorems +print_quotients + +quotient_def + ZERO::"my_int" +where + "ZERO \ (0::nat, 0::nat)" + +ML {* print_qconstinfo @{context} *} + +term ZERO +thm ZERO_def + +ML {* prop_of @{thm ZERO_def} *} + +ML {* separate *} + +quotient_def + ONE::"my_int" +where + "ONE \ (1::nat, 0::nat)" + +ML {* print_qconstinfo @{context} *} + +term ONE +thm ONE_def + +fun + my_plus :: "(nat \ nat) \ (nat \ nat) \ (nat \ nat)" +where + "my_plus (x, y) (u, v) = (x + u, y + v)" + +quotient_def + PLUS::"my_int \ my_int \ my_int" +where + "PLUS \ my_plus" + +term my_plus +term PLUS +thm PLUS_def + +fun + my_neg :: "(nat \ nat) \ (nat \ nat)" +where + "my_neg (x, y) = (y, x)" + +quotient_def + NEG::"my_int \ my_int" +where + "NEG \ my_neg" + +term NEG +thm NEG_def + +definition + MINUS :: "my_int \ my_int \ my_int" +where + "MINUS z w = PLUS z (NEG w)" + +fun + my_mult :: "(nat \ nat) \ (nat \ nat) \ (nat \ nat)" +where + "my_mult (x, y) (u, v) = (x*u + y*v, x*v + y*u)" + +quotient_def + MULT::"my_int \ my_int \ my_int" +where + "MULT \ my_mult" + +term MULT +thm MULT_def + +(* NOT SURE WETHER THIS DEFINITION IS CORRECT *) +fun + my_le :: "(nat \ nat) \ (nat \ nat) \ bool" +where + "my_le (x, y) (u, v) = (x+v \ u+y)" + +quotient_def + LE :: "my_int \ my_int \ bool" +where + "LE \ my_le" + +term LE +thm LE_def + + +definition + LESS :: "my_int \ my_int \ bool" +where + "LESS z w = (LE z w \ z \ w)" + +term LESS +thm LESS_def + +definition + ABS :: "my_int \ my_int" +where + "ABS i = (if (LESS i ZERO) then (NEG i) else i)" + +definition + SIGN :: "my_int \ my_int" +where + "SIGN i = (if i = ZERO then ZERO else if (LESS ZERO i) then ONE else (NEG ONE))" + +ML {* print_qconstinfo @{context} *} + +lemma plus_sym_pre: + shows "my_plus a b \ my_plus b a" + apply(cases a) + apply(cases b) + apply(auto) + done + +lemma plus_rsp[quotient_rsp]: + shows "(intrel ===> intrel ===> intrel) my_plus my_plus" +by (simp) + +ML {* val qty = @{typ "my_int"} *} +ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} +ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "my_int"; *} + +ML {* fun lift_tac_intex lthy t = lift_tac lthy t *} + +ML {* fun inj_repabs_tac_intex lthy = inj_repabs_tac lthy [rel_refl] [trans2] *} +ML {* fun all_inj_repabs_tac_intex lthy = all_inj_repabs_tac lthy [rel_refl] [trans2] *} + +lemma test1: "my_plus a b = my_plus a b" +apply(rule refl) +done + +lemma "PLUS a b = PLUS a b" +apply(tactic {* procedure_tac @{context} @{thm test1} 1 *}) +apply(tactic {* regularize_tac @{context} 1 *}) +apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) +apply(tactic {* clean_tac @{context} 1 *}) +done + +thm lambda_prs + +lemma test2: "my_plus a = my_plus a" +apply(rule refl) +done + +lemma "PLUS a = PLUS a" +apply(tactic {* procedure_tac @{context} @{thm test2} 1 *}) +apply(rule ballI) +apply(rule apply_rsp[OF Quotient_my_int plus_rsp]) +apply(simp only: in_respects) +apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) +apply(tactic {* clean_tac @{context} 1 *}) +done + +lemma test3: "my_plus = my_plus" +apply(rule refl) +done + +lemma "PLUS = PLUS" +apply(tactic {* procedure_tac @{context} @{thm test3} 1 *}) +apply(rule plus_rsp) +apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) +apply(tactic {* clean_tac @{context} 1 *}) +done + + +lemma "PLUS a b = PLUS b a" +apply(tactic {* procedure_tac @{context} @{thm plus_sym_pre} 1 *}) +apply(tactic {* regularize_tac @{context} 1 *}) +apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) +apply(tactic {* clean_tac @{context} 1 *}) +done + +lemma plus_assoc_pre: + shows "my_plus (my_plus i j) k \ my_plus i (my_plus j k)" + apply (cases i) + apply (cases j) + apply (cases k) + apply (simp) + done + +lemma plus_assoc: "PLUS (PLUS x xa) xb = PLUS x (PLUS xa xb)" +apply(tactic {* procedure_tac @{context} @{thm plus_assoc_pre} 1 *}) +apply(tactic {* regularize_tac @{context} 1 *}) +apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) +apply(tactic {* clean_tac @{context} 1 *}) +done + +lemma ho_tst: "foldl my_plus x [] = x" +apply simp +done + +lemma "foldl PLUS x [] = x" +apply(tactic {* procedure_tac @{context} @{thm ho_tst} 1 *}) +apply(tactic {* regularize_tac @{context} 1 *}) +apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) +apply(tactic {* clean_tac @{context} 1 *}) +apply(simp only: foldl_prs[OF Quotient_my_int Quotient_my_int] nil_prs[OF Quotient_my_int]) +done + +lemma ho_tst2: "foldl my_plus x (h # t) \ my_plus h (foldl my_plus x t)" +sorry + +lemma "foldl PLUS x (h # t) = PLUS h (foldl PLUS x t)" +apply(tactic {* procedure_tac @{context} @{thm ho_tst2} 1 *}) +apply(tactic {* regularize_tac @{context} 1 *}) +apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) +apply(tactic {* clean_tac @{context} 1 *}) +apply(simp only: foldl_prs[OF Quotient_my_int Quotient_my_int] cons_prs[OF Quotient_my_int]) +done + +lemma ho_tst3: "foldl f (s::nat \ nat) ([]::(nat \ nat) list) = s" +by simp + +lemma "foldl f (x::my_int) ([]::my_int list) = x" +apply(tactic {* procedure_tac @{context} @{thm ho_tst3} 1 *}) +apply(tactic {* regularize_tac @{context} 1 *}) +apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) +(* TODO: does not work when this is added *) +(* apply(tactic {* lambda_prs_tac @{context} 1 *})*) +apply(tactic {* clean_tac @{context} 1 *}) +apply(simp only: foldl_prs[OF Quotient_my_int Quotient_my_int] nil_prs[OF Quotient_my_int]) +done + +lemma lam_tst: "(\x. (x, x)) y = (y, (y :: nat \ nat))" +by simp + +lemma "(\x. (x, x)) (y::my_int) = (y, y)" +apply(tactic {* procedure_tac @{context} @{thm lam_tst} 1 *}) +apply(tactic {* regularize_tac @{context} 1 *}) +apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) +apply(tactic {* clean_tac @{context} 1 *}) +apply(simp add: pair_prs) +done + +lemma lam_tst2: "(\(y :: nat \ nat). y) = (\(x :: nat \ nat). x)" +by simp + + + + +lemma "(\(y :: my_int). y) = (\(x :: my_int). x)" +apply(tactic {* procedure_tac @{context} @{thm lam_tst2} 1 *}) +defer +apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) +(*apply(tactic {* lambda_prs_tac @{context} 1 *})*) +sorry + +lemma lam_tst3: "(\(y :: nat \ nat \ nat \ nat). y) = (\(x :: nat \ nat \ nat \ nat). x)" +by auto + +lemma "(\(y :: my_int \ my_int). y) = (\(x :: my_int \ my_int). x)" +apply(tactic {* procedure_tac @{context} @{thm lam_tst3} 1 *}) +defer +apply(tactic {* all_inj_repabs_tac_intex @{context} 1*}) +apply(tactic {* lambda_prs_tac @{context} 1 *}) +sorry diff -r 6088fea1c8b1 -r 8a1c8dc72b5c Quot/Examples/IntEx2.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Quot/Examples/IntEx2.thy Mon Dec 07 14:09:50 2009 +0100 @@ -0,0 +1,436 @@ +theory IntEx2 +imports "../QuotMain" +uses + ("Tools/numeral.ML") + ("Tools/numeral_syntax.ML") + ("Tools/int_arith.ML") +begin + + +fun + intrel :: "(nat \ nat) \ (nat \ nat) \ bool" (infix "\" 50) +where + "intrel (x, y) (u, v) = (x + v = u + y)" + +quotient int = "nat \ nat" / intrel + apply(unfold equivp_def) + apply(auto simp add: mem_def expand_fun_eq) + done + +instantiation int :: "{zero, one, plus, minus, uminus, times, ord, abs, sgn}" +begin + +quotient_def + zero_qnt::"int" +where + "zero_qnt \ (0::nat, 0::nat)" + +definition Zero_int_def[code del]: + "0 = zero_qnt" + +quotient_def + one_qnt::"int" +where + "one_qnt \ (1::nat, 0::nat)" + +definition One_int_def[code del]: + "1 = one_qnt" + +fun + plus_raw :: "(nat \ nat) \ (nat \ nat) \ (nat \ nat)" +where + "plus_raw (x, y) (u, v) = (x + u, y + v)" + +quotient_def + plus_qnt::"int \ int \ int" +where + "plus_qnt \ plus_raw" + +definition add_int_def[code del]: + "z + w = plus_qnt z w" + +fun + minus_raw :: "(nat \ nat) \ (nat \ nat)" +where + "minus_raw (x, y) = (y, x)" + +quotient_def + minus_qnt::"int \ int" +where + "minus_qnt \ minus_raw" + +definition minus_int_def [code del]: + "- z = minus_qnt z" + +definition + diff_int_def [code del]: "z - w = z + (-w::int)" + +fun + mult_raw :: "(nat \ nat) \ (nat \ nat) \ (nat \ nat)" +where + "mult_raw (x, y) (u, v) = (x*u + y*v, x*v + y*u)" + +quotient_def + mult_qnt::"int \ int \ int" +where + "mult_qnt \ mult_raw" + +definition + mult_int_def [code del]: "z * w = mult_qnt z w" + +fun + le_raw :: "(nat \ nat) \ (nat \ nat) \ bool" +where + "le_raw (x, y) (u, v) = (x+v \ u+y)" + +quotient_def + le_qnt :: "int \ int \ bool" +where + "le_qnt \ le_raw" + +definition + le_int_def [code del]: + "z \ w = le_qnt z w" + +definition + less_int_def [code del]: "(z\int) < w = (z \ w \ z \ w)" + +definition + zabs_def: "\i\int\ = (if i < 0 then - i else i)" + +definition + zsgn_def: "sgn (i\int) = (if i=0 then 0 else if 0 ===> op \ ===> op \) plus_raw plus_raw" +by auto + +lemma minus_raw_rsp[quotient_rsp]: + shows "(op \ ===> op \) minus_raw minus_raw" + by auto + +lemma mult_raw_rsp[quotient_rsp]: + shows "(op \ ===> op \ ===> op \) mult_raw mult_raw" +apply(auto) +apply(simp add: mult algebra_simps) +sorry + +lemma le_raw_rsp[quotient_rsp]: + shows "(op \ ===> op \ ===> op =) le_raw le_raw" +by auto + +lemma plus_assoc_raw: + shows "plus_raw (plus_raw i j) k \ plus_raw i (plus_raw j k)" +by (cases i, cases j, cases k) (simp) + +lemma plus_sym_raw: + shows "plus_raw i j \ plus_raw j i" +by (cases i, cases j) (simp) + +lemma plus_zero_raw: + shows "plus_raw (0, 0) i \ i" +by (cases i) (simp) + +lemma plus_minus_zero_raw: + shows "plus_raw (minus_raw i) i \ (0, 0)" +by (cases i) (simp) + +lemma mult_assoc_raw: + shows "mult_raw (mult_raw i j) k \ mult_raw i (mult_raw j k)" +by (cases i, cases j, cases k) + (simp add: mult algebra_simps) + +lemma mult_sym_raw: + shows "mult_raw i j \ mult_raw j i" +by (cases i, cases j) (simp) + +lemma mult_one_raw: + shows "mult_raw (1, 0) i \ i" +by (cases i) (simp) + +lemma mult_plus_comm_raw: + shows "mult_raw (plus_raw i j) k \ plus_raw (mult_raw i k) (mult_raw j k)" +by (cases i, cases j, cases k) + (simp add: mult algebra_simps) + +lemma one_zero_distinct: + shows "\ (0, 0) \ ((1::nat), (0::nat))" + by simp + +text{*The integers form a @{text comm_ring_1}*} + + +ML {* val qty = @{typ "int"} *} +ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} +ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "int" *} + +instance int :: comm_ring_1 +proof + fix i j k :: int + show "(i + j) + k = i + (j + k)" + unfolding add_int_def + apply(tactic {* lift_tac @{context} @{thm plus_assoc_raw} 1 *}) + done + show "i + j = j + i" + unfolding add_int_def + apply(tactic {* lift_tac @{context} @{thm plus_sym_raw} 1 *}) + done + show "0 + i = (i::int)" + unfolding add_int_def Zero_int_def + apply(tactic {* lift_tac @{context} @{thm plus_zero_raw} 1 *}) + done + show "- i + i = 0" + unfolding add_int_def minus_int_def Zero_int_def + apply(tactic {* lift_tac @{context} @{thm plus_minus_zero_raw} 1 *}) + done + show "i - j = i + - j" + by (simp add: diff_int_def) + show "(i * j) * k = i * (j * k)" + unfolding mult_int_def + apply(tactic {* lift_tac @{context} @{thm mult_assoc_raw} 1 *}) + done + show "i * j = j * i" + unfolding mult_int_def + apply(tactic {* lift_tac @{context} @{thm mult_sym_raw} 1 *}) + done + show "1 * i = i" + unfolding mult_int_def One_int_def + apply(tactic {* lift_tac @{context} @{thm mult_one_raw} 1 *}) + done + show "(i + j) * k = i * k + j * k" + unfolding mult_int_def add_int_def + apply(tactic {* lift_tac @{context} @{thm mult_plus_comm_raw} 1 *}) + done + show "0 \ (1::int)" + unfolding Zero_int_def One_int_def + apply(tactic {* lift_tac @{context} @{thm one_zero_distinct} 1 *}) + done +qed + +term of_nat +thm of_nat_def + +lemma int_def: "of_nat m = ABS_int (m, 0)" +apply(induct m) +apply(simp add: Zero_int_def zero_qnt_def) +apply(simp) +apply(simp add: add_int_def One_int_def) +apply(simp add: plus_qnt_def one_qnt_def) +oops + +lemma le_antisym_raw: + shows "le_raw i j \ le_raw j i \ i \ j" +by (cases i, cases j) (simp) + +lemma le_refl_raw: + shows "le_raw i i" +by (cases i) (simp) + +lemma le_trans_raw: + shows "le_raw i j \ le_raw j k \ le_raw i k" +by (cases i, cases j, cases k) (simp) + +lemma le_cases_raw: + shows "le_raw i j \ le_raw j i" +by (cases i, cases j) + (simp add: linorder_linear) + +instance int :: linorder +proof + fix i j k :: int + show antisym: "i \ j \ j \ i \ i = j" + unfolding le_int_def + apply(tactic {* lift_tac @{context} @{thm le_antisym_raw} 1 *}) + done + show "(i < j) = (i \ j \ \ j \ i)" + by (auto simp add: less_int_def dest: antisym) + show "i \ i" + unfolding le_int_def + apply(tactic {* lift_tac @{context} @{thm le_refl_raw} 1 *}) + done + show "i \ j \ j \ k \ i \ k" + unfolding le_int_def + apply(tactic {* lift_tac @{context} @{thm le_trans_raw} 1 *}) + done + show "i \ j \ j \ i" + unfolding le_int_def + apply(tactic {* lift_tac @{context} @{thm le_cases_raw} 1 *}) + done +qed + +instantiation int :: distrib_lattice +begin + +definition + "(inf \ int \ int \ int) = min" + +definition + "(sup \ int \ int \ int) = max" + +instance + by intro_classes + (auto simp add: inf_int_def sup_int_def min_max.sup_inf_distrib1) + +end + +lemma le_plus_raw: + shows "le_raw i j \ le_raw (plus_raw k i) (plus_raw k j)" +by (cases i, cases j, cases k) (simp) + + +instance int :: pordered_cancel_ab_semigroup_add +proof + fix i j k :: int + show "i \ j \ k + i \ k + j" + unfolding le_int_def add_int_def + apply(tactic {* lift_tac @{context} @{thm le_plus_raw} 1 *}) + done +qed + +lemma test: + "\le_raw i j \ \i \ j; le_raw (0, 0) k \ \(0, 0) \ k\ + \ le_raw (mult_raw k i) (mult_raw k j) \ \mult_raw k i \ mult_raw k j" +apply(cases i, cases j, cases k) +apply(auto simp add: mult algebra_simps) +sorry + + +text{*The integers form an ordered integral domain*} +instance int :: ordered_idom +proof + fix i j k :: int + show "i < j \ 0 < k \ k * i < k * j" + unfolding mult_int_def le_int_def less_int_def Zero_int_def + apply(tactic {* lift_tac @{context} @{thm test} 1 *}) + done + show "\i\ = (if i < 0 then -i else i)" + by (simp only: zabs_def) + show "sgn (i\int) = (if i=0 then 0 else if 0 'a" +where + "of_int +*) + + +subsection {* Binary representation *} + +text {* + This formalization defines binary arithmetic in terms of the integers + rather than using a datatype. This avoids multiple representations (leading + zeroes, etc.) See @{text "ZF/Tools/twos-compl.ML"}, function @{text + int_of_binary}, for the numerical interpretation. + + The representation expects that @{text "(m mod 2)"} is 0 or 1, + even if m is negative; + For instance, @{text "-5 div 2 = -3"} and @{text "-5 mod 2 = 1"}; thus + @{text "-5 = (-3)*2 + 1"}. + + This two's complement binary representation derives from the paper + "An Efficient Representation of Arithmetic for Term Rewriting" by + Dave Cohen and Phil Watson, Rewriting Techniques and Applications, + Springer LNCS 488 (240-251), 1991. +*} + +subsubsection {* The constructors @{term Bit0}, @{term Bit1}, @{term Pls} and @{term Min} *} + +definition + Pls :: int where + [code del]: "Pls = 0" + +definition + Min :: int where + [code del]: "Min = - 1" + +definition + Bit0 :: "int \ int" where + [code del]: "Bit0 k = k + k" + +definition + Bit1 :: "int \ int" where + [code del]: "Bit1 k = 1 + k + k" + +class number = -- {* for numeric types: nat, int, real, \dots *} + fixes number_of :: "int \ 'a" + +use "~~/src/HOL/Tools/numeral.ML" + +syntax + "_Numeral" :: "num_const \ 'a" ("_") + +use "~~/src/HOL/Tools/numeral_syntax.ML" +(* +setup NumeralSyntax.setup + +abbreviation + "Numeral0 \ number_of Pls" + +abbreviation + "Numeral1 \ number_of (Bit1 Pls)" + +lemma Let_number_of [simp]: "Let (number_of v) f = f (number_of v)" + -- {* Unfold all @{text let}s involving constants *} + unfolding Let_def .. + +definition + succ :: "int \ int" where + [code del]: "succ k = k + 1" + +definition + pred :: "int \ int" where + [code del]: "pred k = k - 1" + +lemmas + max_number_of [simp] = max_def + [of "number_of u" "number_of v", standard, simp] +and + min_number_of [simp] = min_def + [of "number_of u" "number_of v", standard, simp] + -- {* unfolding @{text minx} and @{text max} on numerals *} + +lemmas numeral_simps = + succ_def pred_def Pls_def Min_def Bit0_def Bit1_def + +text {* Removal of leading zeroes *} + +lemma Bit0_Pls [simp, code_post]: + "Bit0 Pls = Pls" + unfolding numeral_simps by simp + +lemma Bit1_Min [simp, code_post]: + "Bit1 Min = Min" + unfolding numeral_simps by simp + +lemmas normalize_bin_simps = + Bit0_Pls Bit1_Min +*) \ No newline at end of file diff -r 6088fea1c8b1 -r 8a1c8dc72b5c Quot/Examples/LFex.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Quot/Examples/LFex.thy Mon Dec 07 14:09:50 2009 +0100 @@ -0,0 +1,307 @@ +theory LFex +imports Nominal "../QuotMain" +begin + +atom_decl name ident + +nominal_datatype kind = + Type + | KPi "ty" "name" "kind" +and ty = + TConst "ident" + | TApp "ty" "trm" + | TPi "ty" "name" "ty" +and trm = + Const "ident" + | Var "name" + | App "trm" "trm" + | Lam "ty" "name" "trm" + +function + fv_kind :: "kind \ name set" +and fv_ty :: "ty \ name set" +and fv_trm :: "trm \ name set" +where + "fv_kind (Type) = {}" +| "fv_kind (KPi A x K) = (fv_ty A) \ ((fv_kind K) - {x})" +| "fv_ty (TConst i) = {}" +| "fv_ty (TApp A M) = (fv_ty A) \ (fv_trm M)" +| "fv_ty (TPi A x B) = (fv_ty A) \ ((fv_ty B) - {x})" +| "fv_trm (Const i) = {}" +| "fv_trm (Var x) = {x}" +| "fv_trm (App M N) = (fv_trm M) \ (fv_trm N)" +| "fv_trm (Lam A x M) = (fv_ty A) \ ((fv_trm M) - {x})" +sorry + +termination fv_kind sorry + +inductive + akind :: "kind \ kind \ bool" ("_ \ki _" [100, 100] 100) +and aty :: "ty \ ty \ bool" ("_ \ty _" [100, 100] 100) +and atrm :: "trm \ trm \ bool" ("_ \tr _" [100, 100] 100) +where + a1: "(Type) \ki (Type)" +| a21: "\A \ty A'; K \ki K'\ \ (KPi A x K) \ki (KPi A' x K')" +| a22: "\A \ty A'; K \ki ([(x,x')]\K'); x \ (fv_ty A'); x \ ((fv_kind K') - {x'})\ + \ (KPi A x K) \ki (KPi A' x' K')" +| a3: "i = j \ (TConst i) \ty (TConst j)" +| a4: "\A \ty A'; M \tr M'\ \ (TApp A M) \ty (TApp A' M')" +| a51: "\A \ty A'; B \ty B'\ \ (TPi A x B) \ty (TPi A' x B')" +| a52: "\A \ty A'; B \ty ([(x,x')]\B'); x \ (fv_ty B'); x \ ((fv_ty B') - {x'})\ + \ (TPi A x B) \ty (TPi A' x' B')" +| a6: "i = j \ (Const i) \trm (Const j)" +| a7: "x = y \ (Var x) \trm (Var y)" +| a8: "\M \trm M'; N \tr N'\ \ (App M N) \tr (App M' N')" +| a91: "\A \ty A'; M \tr M'\ \ (Lam A x M) \tr (Lam A' x M')" +| a92: "\A \ty A'; M \tr ([(x,x')]\M'); x \ (fv_ty B'); x \ ((fv_trm M') - {x'})\ + \ (Lam A x M) \tr (Lam A' x' M')" + +lemma al_refl: + fixes K::"kind" + and A::"ty" + and M::"trm" + shows "K \ki K" + and "A \ty A" + and "M \tr M" + apply(induct K and A and M rule: kind_ty_trm.inducts) + apply(auto intro: akind_aty_atrm.intros) + done + +lemma alpha_equivps: + shows "equivp akind" + and "equivp aty" + and "equivp atrm" +sorry + +quotient KIND = kind / akind + by (rule alpha_equivps) + +quotient TY = ty / aty + and TRM = trm / atrm + by (auto intro: alpha_equivps) + +print_quotients + +quotient_def + TYP :: "KIND" +where + "TYP \ Type" + +quotient_def + KPI :: "TY \ name \ KIND \ KIND" +where + "KPI \ KPi" + +quotient_def + TCONST :: "ident \ TY" +where + "TCONST \ TConst" + +quotient_def + TAPP :: "TY \ TRM \ TY" +where + "TAPP \ TApp" + +quotient_def + TPI :: "TY \ name \ TY \ TY" +where + "TPI \ TPi" + +(* FIXME: does not work with CONST *) +quotient_def + CONS :: "ident \ TRM" +where + "CONS \ Const" + +quotient_def + VAR :: "name \ TRM" +where + "VAR \ Var" + +quotient_def + APP :: "TRM \ TRM \ TRM" +where + "APP \ App" + +quotient_def + LAM :: "TY \ name \ TRM \ TRM" +where + "LAM \ Lam" + +thm TYP_def +thm KPI_def +thm TCONST_def +thm TAPP_def +thm TPI_def +thm VAR_def +thm CONS_def +thm APP_def +thm LAM_def + +(* FIXME: print out a warning if the type contains a liftet type, like kind \ name set *) +quotient_def + FV_kind :: "KIND \ name set" +where + "FV_kind \ fv_kind" + +quotient_def + FV_ty :: "TY \ name set" +where + "FV_ty \ fv_ty" + +quotient_def + FV_trm :: "TRM \ name set" +where + "FV_trm \ fv_trm" + +thm FV_kind_def +thm FV_ty_def +thm FV_trm_def + +(* FIXME: does not work yet *) +overloading + perm_kind \ "perm :: 'x prm \ KIND \ KIND" (unchecked) + perm_ty \ "perm :: 'x prm \ TY \ TY" (unchecked) + perm_trm \ "perm :: 'x prm \ TRM \ TRM" (unchecked) +begin + +quotient_def + perm_kind :: "'x prm \ KIND \ KIND" +where + "perm_kind \ (perm::'x prm \ kind \ kind)" + +quotient_def + perm_ty :: "'x prm \ TY \ TY" +where + "perm_ty \ (perm::'x prm \ ty \ ty)" + +quotient_def + perm_trm :: "'x prm \ TRM \ TRM" +where + "perm_trm \ (perm::'x prm \ trm \ trm)" + +(* TODO/FIXME: Think whether these RSP theorems are true. *) +lemma kpi_rsp[quotient_rsp]: + "(aty ===> op = ===> akind ===> akind) KPi KPi" sorry +lemma tconst_rsp[quotient_rsp]: + "(op = ===> aty) TConst TConst" sorry +lemma tapp_rsp[quotient_rsp]: + "(aty ===> atrm ===> aty) TApp TApp" sorry +lemma tpi_rsp[quotient_rsp]: + "(aty ===> op = ===> aty ===> aty) TPi TPi" sorry +lemma var_rsp[quotient_rsp]: + "(op = ===> atrm) Var Var" sorry +lemma app_rsp[quotient_rsp]: + "(atrm ===> atrm ===> atrm) App App" sorry +lemma const_rsp[quotient_rsp]: + "(op = ===> atrm) Const Const" sorry +lemma lam_rsp[quotient_rsp]: + "(aty ===> op = ===> atrm ===> atrm) Lam Lam" sorry + +lemma perm_kind_rsp[quotient_rsp]: + "(op = ===> akind ===> akind) op \ op \" sorry +lemma perm_ty_rsp[quotient_rsp]: + "(op = ===> aty ===> aty) op \ op \" sorry +lemma perm_trm_rsp[quotient_rsp]: + "(op = ===> atrm ===> atrm) op \ op \" sorry + +lemma fv_ty_rsp[quotient_rsp]: + "(aty ===> op =) fv_ty fv_ty" sorry +lemma fv_kind_rsp[quotient_rsp]: + "(akind ===> op =) fv_kind fv_kind" sorry +lemma fv_trm_rsp[quotient_rsp]: + "(atrm ===> op =) fv_trm fv_trm" sorry + + +thm akind_aty_atrm.induct +thm kind_ty_trm.induct + +ML {* + val quot = @{thms Quotient_KIND Quotient_TY Quotient_TRM} + val rel_refl = map (fn x => @{thm equivp_reflp} OF [x]) @{thms alpha_equivps} + val reps_same = map (fn x => @{thm Quotient_rel_rep} OF [x]) quot + val trans2 = map (fn x => @{thm equals_rsp} OF [x]) quot +*} + +lemma + assumes a0: + "P1 TYP TYP" + and a1: + "\A A' K K' x. \(A::TY) = A'; P2 A A'; (K::KIND) = K'; P1 K K'\ + \ P1 (KPI A x K) (KPI A' x K')" + and a2: + "\A A' K K' x x'. \(A ::TY) = A'; P2 A A'; (K :: KIND) = ([(x, x')] \ K'); P1 K ([(x, x')] \ K'); + x \ FV_ty A'; x \ FV_kind K' - {x'}\ \ P1 (KPI A x K) (KPI A' x' K')" + and a3: + "\i j. i = j \ P2 (TCONST i) (TCONST j)" + and a4: + "\A A' M M'. \(A ::TY) = A'; P2 A A'; (M :: TRM) = M'; P3 M M'\ \ P2 (TAPP A M) (TAPP A' M')" + and a5: + "\A A' B B' x. \(A ::TY) = A'; P2 A A'; (B ::TY) = B'; P2 B B'\ \ P2 (TPI A x B) (TPI A' x B')" + and a6: + "\A A' B x x' B'. \(A ::TY) = A'; P2 A A'; (B ::TY) = ([(x, x')] \ B'); P2 B ([(x, x')] \ B'); + x \ FV_ty B'; x \ FV_ty B' - {x'}\ \ P2 (TPI A x B) (TPI A' x' B')" + and a7: + "\i j m. i = j \ P3 (CONS i) (m (CONS j))" + and a8: + "\x y m. x = y \ P3 (VAR x) (m (VAR y))" + and a9: + "\M m M' N N'. \(M :: TRM) = m M'; P3 M (m M'); (N :: TRM) = N'; P3 N N'\ \ P3 (APP M N) (APP M' N')" + and a10: + "\A A' M M' x. \(A ::TY) = A'; P2 A A'; (M :: TRM) = M'; P3 M M'\ \ P3 (LAM A x M) (LAM A' x M')" + and a11: + "\A A' M x x' M' B'. \(A ::TY) = A'; P2 A A'; (M :: TRM) = ([(x, x')] \ M'); P3 M ([(x, x')] \ M'); + x \ FV_ty B'; x \ FV_trm M' - {x'}\ \ P3 (LAM A x M) (LAM A' x' M')" + shows "((x1 :: KIND) = x2 \ P1 x1 x2) \ + ((x3 ::TY) = x4 \ P2 x3 x4) \ + ((x5 :: TRM) = x6 \ P3 x5 x6)" +using a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 +apply - +apply(tactic {* procedure_tac @{context} @{thm akind_aty_atrm.induct} 1 *}) +apply(tactic {* regularize_tac @{context} 1 *}) +apply(tactic {* all_inj_repabs_tac @{context} rel_refl trans2 1 *}) +apply(fold perm_kind_def perm_ty_def perm_trm_def) +apply(tactic {* clean_tac @{context} 1 *}) +(* +Profiling: +ML_prf {* fun ith i = (#concl (fst (Subgoal.focus @{context} i (#goal (Isar.goal ()))))) *} +ML_prf {* profile 2 Seq.list_of ((clean_tac @{context} quot defs 1) (ith 3)) *} +ML_prf {* profile 2 Seq.list_of ((regularize_tac @{context} @{thms alpha_equivps} 1) (ith 1)) *} +ML_prf {* PolyML.profiling 1 *} +ML_prf {* profile 2 Seq.list_of ((all_inj_repabs_tac @{context} quot rel_refl trans2 1) (#goal (Isar.goal ()))) *} +*) +done + +(* Does not work: +lemma + assumes a0: "P1 TYP" + and a1: "\ty name kind. \P2 ty; P1 kind\ \ P1 (KPI ty name kind)" + and a2: "\id. P2 (TCONST id)" + and a3: "\ty trm. \P2 ty; P3 trm\ \ P2 (TAPP ty trm)" + and a4: "\ty1 name ty2. \P2 ty1; P2 ty2\ \ P2 (TPI ty1 name ty2)" + and a5: "\id. P3 (CONS id)" + and a6: "\name. P3 (VAR name)" + and a7: "\trm1 trm2. \P3 trm1; P3 trm2\ \ P3 (APP trm1 trm2)" + and a8: "\ty name trm. \P2 ty; P3 trm\ \ P3 (LAM ty name trm)" + shows "P1 mkind \ P2 mty \ P3 mtrm" +using a0 a1 a2 a3 a4 a5 a6 a7 a8 +*) + +lemma "\P TYP; + \ty name kind. \Q ty; P kind\ \ P (KPI ty name kind); + \id. Q (TCONST id); + \ty trm. \Q ty; R trm\ \ Q (TAPP ty trm); + \ty1 name ty2. \Q ty1; Q ty2\ \ Q (TPI ty1 name ty2); + \id. R (CONS id); \name. R (VAR name); + \trm1 trm2. \R trm1; R trm2\ \ R (APP trm1 trm2); + \ty name trm. \Q ty; R trm\ \ R (LAM ty name trm)\ + \ P mkind \ Q mty \ R mtrm" +apply(tactic {* lift_tac @{context} @{thm kind_ty_trm.induct} 1 *}) +done + +print_quotients + +end + + + diff -r 6088fea1c8b1 -r 8a1c8dc72b5c Quot/Examples/LamEx.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Quot/Examples/LamEx.thy Mon Dec 07 14:09:50 2009 +0100 @@ -0,0 +1,252 @@ +theory LamEx +imports Nominal "../QuotMain" +begin + +atom_decl name + +thm abs_fresh(1) + +nominal_datatype rlam = + rVar "name" +| rApp "rlam" "rlam" +| rLam "name" "rlam" + +print_theorems + +function + rfv :: "rlam \ name set" +where + rfv_var: "rfv (rVar a) = {a}" +| rfv_app: "rfv (rApp t1 t2) = (rfv t1) \ (rfv t2)" +| rfv_lam: "rfv (rLam a t) = (rfv t) - {a}" +sorry + +termination rfv sorry + +inductive + alpha :: "rlam \ rlam \ bool" ("_ \ _" [100, 100] 100) +where + a1: "a = b \ (rVar a) \ (rVar b)" +| a2: "\t1 \ t2; s1 \ s2\ \ rApp t1 s1 \ rApp t2 s2" +| a3: "\t \ ([(a,b)]\s); a \ rfv (rLam b t)\ \ rLam a t \ rLam b s" + +print_theorems + +lemma alpha_refl: + fixes t::"rlam" + shows "t \ t" + apply(induct t rule: rlam.induct) + apply(simp add: a1) + apply(simp add: a2) + apply(rule a3) + apply(subst pt_swap_bij'') + apply(rule pt_name_inst) + apply(rule at_name_inst) + apply(simp) + apply(simp) + done + +lemma alpha_equivp: + shows "equivp alpha" +sorry + +quotient lam = rlam / alpha + apply(rule alpha_equivp) + done + +print_quotients + +quotient_def + Var :: "name \ lam" +where + "Var \ rVar" + +quotient_def + App :: "lam \ lam \ lam" +where + "App \ rApp" + +quotient_def + Lam :: "name \ lam \ lam" +where + "Lam \ rLam" + +thm Var_def +thm App_def +thm Lam_def + +quotient_def + fv :: "lam \ name set" +where + "fv \ rfv" + +thm fv_def + +(* definition of overloaded permutation function *) +(* for the lifted type lam *) +overloading + perm_lam \ "perm :: 'x prm \ lam \ lam" (unchecked) +begin + +quotient_def + perm_lam :: "'x prm \ lam \ lam" +where + "perm_lam \ (perm::'x prm \ rlam \ rlam)" + +end + +(*quotient_def (for lam) + abs_fun_lam :: "'x prm \ lam \ lam" +where + "perm_lam \ (perm::'x prm \ rlam \ rlam)"*) + + +thm perm_lam_def + +(* lemmas that need to lift *) +lemma pi_var_com: + fixes pi::"'x prm" + shows "(pi\rVar a) \ rVar (pi\a)" + sorry + +lemma pi_app_com: + fixes pi::"'x prm" + shows "(pi\rApp t1 t2) \ rApp (pi\t1) (pi\t2)" + sorry + +lemma pi_lam_com: + fixes pi::"'x prm" + shows "(pi\rLam a t) \ rLam (pi\a) (pi\t)" + sorry + + + +lemma real_alpha: + assumes a: "t = [(a,b)]\s" "a\[b].s" + shows "Lam a t = Lam b s" +using a +unfolding fresh_def supp_def +sorry + +lemma perm_rsp[quotient_rsp]: + "(op = ===> alpha ===> alpha) op \ op \" + apply(auto) + (* this is propably true if some type conditions are imposed ;o) *) + sorry + +lemma fresh_rsp: + "(op = ===> alpha ===> op =) fresh fresh" + apply(auto) + (* this is probably only true if some type conditions are imposed *) + sorry + +lemma rVar_rsp[quotient_rsp]: + "(op = ===> alpha) rVar rVar" +by (auto intro:a1) + +lemma rApp_rsp[quotient_rsp]: "(alpha ===> alpha ===> alpha) rApp rApp" +by (auto intro:a2) + +lemma rLam_rsp[quotient_rsp]: "(op = ===> alpha ===> alpha) rLam rLam" + apply(auto) + apply(rule a3) + apply(rule_tac t="[(x,x)]\y" and s="y" in subst) + apply(rule sym) + apply(rule trans) + apply(rule pt_name3) + apply(rule at_ds1[OF at_name_inst]) + apply(simp add: pt_name1) + apply(assumption) + apply(simp add: abs_fresh) + done + +lemma rfv_rsp[quotient_rsp]: "(alpha ===> op =) rfv rfv" + sorry + +lemma rvar_inject: "rVar a \ rVar b = (a = b)" +apply (auto) +apply (erule alpha.cases) +apply (simp_all add: rlam.inject alpha_refl) +done + +ML {* val qty = @{typ "lam"} *} +ML {* val rsp_thms = @{thms perm_rsp fresh_rsp rVar_rsp rApp_rsp rLam_rsp rfv_rsp} *} + +ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} +ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "lam" *} +ML {* fun lift_tac_lam lthy t = lift_tac lthy t *} + +lemma pi_var: "(pi\('x \ 'x) list) \ Var a = Var (pi \ a)" +apply (tactic {* lift_tac_lam @{context} @{thm pi_var_com} 1 *}) +done + +lemma pi_app: "(pi\('x \ 'x) list) \ App (x\lam) (xa\lam) = App (pi \ x) (pi \ xa)" +apply (tactic {* lift_tac_lam @{context} @{thm pi_app_com} 1 *}) +done + +lemma pi_lam: "(pi\('x \ 'x) list) \ Lam (a\name) (x\lam) = Lam (pi \ a) (pi \ x)" +apply (tactic {* lift_tac_lam @{context} @{thm pi_lam_com} 1 *}) +done + +lemma fv_var: "fv (Var (a\name)) = {a}" +apply (tactic {* lift_tac_lam @{context} @{thm rfv_var} 1 *}) +done + +lemma fv_app: "fv (App (x\lam) (xa\lam)) = fv x \ fv xa" +apply (tactic {* lift_tac_lam @{context} @{thm rfv_app} 1 *}) +done + +lemma fv_lam: "fv (Lam (a\name) (x\lam)) = fv x - {a}" +apply (tactic {* lift_tac_lam @{context} @{thm rfv_lam} 1 *}) +done + +lemma a1: "(a\name) = (b\name) \ Var a = Var b" +apply (tactic {* lift_tac_lam @{context} @{thm a1} 1 *}) +done + +lemma a2: "\(x\lam) = (xa\lam); (xb\lam) = (xc\lam)\ \ App x xb = App xa xc" +apply (tactic {* lift_tac_lam @{context} @{thm a2} 1 *}) +done + +lemma a3: "\(x\lam) = [(a\name, b\name)] \ (xa\lam); a \ fv (Lam b x)\ \ Lam a x = Lam b xa" +apply (tactic {* lift_tac_lam @{context} @{thm a3} 1 *}) +done + +lemma alpha_cases: "\a1 = a2; \a b. \a1 = Var a; a2 = Var b; a = b\ \ P; + \x xa xb xc. \a1 = App x xb; a2 = App xa xc; x = xa; xb = xc\ \ P; + \x a b xa. \a1 = Lam a x; a2 = Lam b xa; x = [(a, b)] \ xa; a \ fv (Lam b x)\ \ P\ + \ P" +apply (tactic {* lift_tac_lam @{context} @{thm alpha.cases} 1 *}) +done + +lemma alpha_induct: "\(qx\lam) = (qxa\lam); \(a\name) b\name. a = b \ (qxb\lam \ lam \ bool) (Var a) (Var b); + \(x\lam) (xa\lam) (xb\lam) xc\lam. \x = xa; qxb x xa; xb = xc; qxb xb xc\ \ qxb (App x xb) (App xa xc); + \(x\lam) (a\name) (b\name) xa\lam. + \x = [(a, b)] \ xa; qxb x ([(a, b)] \ xa); a \ fv (Lam b x)\ \ qxb (Lam a x) (Lam b xa)\ + \ qxb qx qxa" +apply (tactic {* lift_tac_lam @{context} @{thm alpha.induct} 1 *}) +done + +lemma var_inject: "(Var a = Var b) = (a = b)" +apply (tactic {* lift_tac_lam @{context} @{thm rvar_inject} 1 *}) +done + +lemma lam_induct:" \\name. P (Var name); \lam1 lam2. \P lam1; P lam2\ \ P (App lam1 lam2); + \name lam. P lam \ P (Lam name lam)\ \ P lam" +apply (tactic {* lift_tac_lam @{context} @{thm rlam.induct} 1 *}) +done + +lemma var_supp: + shows "supp (Var a) = ((supp a)::name set)" + apply(simp add: supp_def) + apply(simp add: pi_var) + apply(simp add: var_inject) + done + +lemma var_fresh: + fixes a::"name" + shows "(a\(Var b)) = (a\b)" + apply(simp add: fresh_def) + apply(simp add: var_supp) + done + diff -r 6088fea1c8b1 -r 8a1c8dc72b5c Quot/Prove.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Quot/Prove.thy Mon Dec 07 14:09:50 2009 +0100 @@ -0,0 +1,28 @@ +theory Prove +imports Plain +begin + +ML {* +val r = Unsynchronized.ref (NONE:(unit -> term) option) +*} + +ML {* +let + fun after_qed thm_name thms lthy = + Local_Theory.note (thm_name, (flat thms)) lthy |> snd + + fun setup_proof (name_spec, (txt, pos)) lthy = + let + val trm = ML_Context.evaluate lthy true ("r", r) txt + in + Proof.theorem_i NONE (after_qed name_spec) [[(trm,[])]] lthy + end + + val parser = SpecParse.opt_thm_name ":" -- OuterParse.ML_source +in + OuterSyntax.local_theory_to_proof "prove" "proving a proposition" + OuterKeyword.thy_goal (parser >> setup_proof) +end +*} + +end diff -r 6088fea1c8b1 -r 8a1c8dc72b5c Quot/QuotList.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Quot/QuotList.thy Mon Dec 07 14:09:50 2009 +0100 @@ -0,0 +1,174 @@ +theory QuotList +imports QuotScript List +begin + +fun + list_rel +where + "list_rel R [] [] = True" +| "list_rel R (x#xs) [] = False" +| "list_rel R [] (x#xs) = False" +| "list_rel R (x#xs) (y#ys) = (R x y \ list_rel R xs ys)" + +lemma list_equivp: + assumes a: "equivp R" + shows "equivp (list_rel R)" + unfolding equivp_def + apply(rule allI)+ + apply(induct_tac x y rule: list_induct2') + apply(simp_all add: expand_fun_eq) + apply(metis list_rel.simps(1) list_rel.simps(2)) + apply(metis list_rel.simps(1) list_rel.simps(2)) + apply(rule iffI) + apply(rule allI) + apply(case_tac x) + apply(simp_all) + using a + apply(unfold equivp_def) + apply(auto)[1] + apply(metis list_rel.simps(4)) + done + +lemma list_rel_rel: + assumes q: "Quotient R Abs Rep" + shows "list_rel R r s = (list_rel R r r \ list_rel R s s \ (map Abs r = map Abs s))" + apply(induct r s rule: list_induct2') + apply(simp_all) + using Quotient_rel[OF q] + apply(metis) + done + +lemma list_quotient: + assumes q: "Quotient R Abs Rep" + shows "Quotient (list_rel R) (map Abs) (map Rep)" + unfolding Quotient_def + apply(rule conjI) + apply(rule allI) + apply(induct_tac a) + apply(simp) + apply(simp add: Quotient_abs_rep[OF q]) + apply(rule conjI) + apply(rule allI) + apply(induct_tac a) + apply(simp) + apply(simp) + apply(simp add: Quotient_rep_reflp[OF q]) + apply(rule allI)+ + apply(rule list_rel_rel[OF q]) + done + + +lemma cons_prs: + assumes q: "Quotient R Abs Rep" + shows "(map Abs) ((Rep h) # (map Rep t)) = h # t" +by (induct t) (simp_all add: Quotient_abs_rep[OF q]) + +lemma cons_rsp: + assumes q: "Quotient R Abs Rep" + shows "(R ===> list_rel R ===> list_rel R) op # op #" +by (auto) + +lemma nil_prs: + assumes q: "Quotient R Abs Rep" + shows "map Abs [] \ []" +by (simp) + +lemma nil_rsp: + assumes q: "Quotient R Abs Rep" + shows "list_rel R [] []" +by simp + +lemma map_prs: + assumes a: "Quotient R1 abs1 rep1" + and b: "Quotient R2 abs2 rep2" + shows "(map abs2) (map ((abs1 ---> rep2) f) (map rep1 l)) = map f l" +by (induct l) (simp_all add: Quotient_abs_rep[OF a] Quotient_abs_rep[OF b]) + +lemma map_rsp: + assumes q1: "Quotient R1 Abs1 Rep1" + and q2: "Quotient R2 Abs2 Rep2" + shows "((R1 ===> R2) ===> (list_rel R1) ===> list_rel R2) map map" +apply(simp) +apply(rule allI)+ +apply(rule impI) +apply(rule allI)+ +apply (induct_tac xa ya rule: list_induct2') +apply simp_all +done + +(* TODO: if the above is correct, we can remove this one *) +lemma map_rsp_lo: + assumes q1: "Quotient R1 Abs1 Rep1" + and q2: "Quotient R2 Abs2 Rep2" + and a: "(R1 ===> R2) f1 f2" + and b: "list_rel R1 l1 l2" + shows "list_rel R2 (map f1 l1) (map f2 l2)" +using b a +by (induct l1 l2 rule: list_induct2') (simp_all) + +lemma foldr_prs: + assumes a: "Quotient R1 abs1 rep1" + and b: "Quotient R2 abs2 rep2" + shows "abs2 (foldr ((abs1 ---> abs2 ---> rep2) f) (map rep1 l) (rep2 e)) = foldr f l e" +by (induct l) (simp_all add: Quotient_abs_rep[OF a] Quotient_abs_rep[OF b]) + +lemma foldl_prs: + assumes a: "Quotient R1 abs1 rep1" + and b: "Quotient R2 abs2 rep2" + shows "abs1 (foldl ((abs1 ---> abs2 ---> rep1) f) (rep1 e) (map rep2 l)) = foldl f e l" +by (induct l arbitrary:e) (simp_all add: Quotient_abs_rep[OF a] Quotient_abs_rep[OF b]) + +lemma list_rel_empty: "list_rel R [] b \ length b = 0" +by (induct b) (simp_all) + +lemma list_rel_len: "list_rel R a b \ length a = length b" +apply (induct a arbitrary: b) +apply (simp add: list_rel_empty) +apply (case_tac b) +apply simp_all +done + +(* TODO: induct_tac doesn't accept 'arbitrary'. + induct doesn't accept 'rule'. + that's why the proof uses manual generalisation and needs assumptions + both in conclusion for induction and in assumptions. *) +lemma foldl_rsp: + assumes q1: "Quotient R1 Abs1 Rep1" + and q2: "Quotient R2 Abs2 Rep2" + shows "((R1 ===> R2 ===> R1) ===> R1 ===> list_rel R2 ===> R1) foldl foldl" +apply auto +apply (subgoal_tac "R1 xa ya \ list_rel R2 xb yb \ R1 (foldl x xa xb) (foldl y ya yb)") +apply simp +apply (rule_tac x="xa" in spec) +apply (rule_tac x="ya" in spec) +apply (rule_tac xs="xb" and ys="yb" in list_induct2) +apply (rule list_rel_len) +apply (simp_all) +done + +(* TODO: foldr_rsp should be similar *) + + + + +(* TODO: Rest are unused *) + +lemma list_map_id: + shows "map (\x. x) = (\x. x)" + by simp + +lemma list_rel_eq: + shows "list_rel (op =) \ (op =)" +apply(rule eq_reflection) +unfolding expand_fun_eq +apply(rule allI)+ +apply(induct_tac x xa rule: list_induct2') +apply(simp_all) +done + +lemma list_rel_refl: + assumes a: "\x y. R x y = (R x = R y)" + shows "list_rel R x x" +by (induct x) (auto simp add: a) + +end diff -r 6088fea1c8b1 -r 8a1c8dc72b5c Quot/QuotMain.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Quot/QuotMain.thy Mon Dec 07 14:09:50 2009 +0100 @@ -0,0 +1,1191 @@ +theory QuotMain +imports QuotScript QuotList QuotProd Prove +uses ("quotient_info.ML") + ("quotient.ML") + ("quotient_def.ML") +begin + + +locale QUOT_TYPE = + fixes R :: "'a \ 'a \ bool" + and Abs :: "('a \ bool) \ 'b" + and Rep :: "'b \ ('a \ bool)" + assumes equivp: "equivp R" + and rep_prop: "\y. \x. Rep y = R x" + and rep_inverse: "\x. Abs (Rep x) = x" + and abs_inverse: "\x. (Rep (Abs (R x))) = (R x)" + and rep_inject: "\x y. (Rep x = Rep y) = (x = y)" +begin + +definition + ABS::"'a \ 'b" +where + "ABS x \ Abs (R x)" + +definition + REP::"'b \ 'a" +where + "REP a = Eps (Rep a)" + +lemma lem9: + shows "R (Eps (R x)) = R x" +proof - + have a: "R x x" using equivp by (simp add: equivp_reflp_symp_transp reflp_def) + then have "R x (Eps (R x))" by (rule someI) + then show "R (Eps (R x)) = R x" + using equivp unfolding equivp_def by simp +qed + +theorem thm10: + shows "ABS (REP a) \ a" + apply (rule eq_reflection) + unfolding ABS_def REP_def +proof - + from rep_prop + obtain x where eq: "Rep a = R x" by auto + have "Abs (R (Eps (Rep a))) = Abs (R (Eps (R x)))" using eq by simp + also have "\ = Abs (R x)" using lem9 by simp + also have "\ = Abs (Rep a)" using eq by simp + also have "\ = a" using rep_inverse by simp + finally + show "Abs (R (Eps (Rep a))) = a" by simp +qed + +lemma REP_refl: + shows "R (REP a) (REP a)" +unfolding REP_def +by (simp add: equivp[simplified equivp_def]) + +lemma lem7: + shows "(R x = R y) = (Abs (R x) = Abs (R y))" +apply(rule iffI) +apply(simp) +apply(drule rep_inject[THEN iffD2]) +apply(simp add: abs_inverse) +done + +theorem thm11: + shows "R r r' = (ABS r = ABS r')" +unfolding ABS_def +by (simp only: equivp[simplified equivp_def] lem7) + + +lemma REP_ABS_rsp: + shows "R f (REP (ABS g)) = R f g" + and "R (REP (ABS g)) f = R g f" +by (simp_all add: thm10 thm11) + +lemma Quotient: + "Quotient R ABS REP" +apply(unfold Quotient_def) +apply(simp add: thm10) +apply(simp add: REP_refl) +apply(subst thm11[symmetric]) +apply(simp add: equivp[simplified equivp_def]) +done + +lemma R_trans: + assumes ab: "R a b" + and bc: "R b c" + shows "R a c" +proof - + have tr: "transp R" using equivp equivp_reflp_symp_transp[of R] by simp + moreover have ab: "R a b" by fact + moreover have bc: "R b c" by fact + ultimately show "R a c" unfolding transp_def by blast +qed + +lemma R_sym: + assumes ab: "R a b" + shows "R b a" +proof - + have re: "symp R" using equivp equivp_reflp_symp_transp[of R] by simp + then show "R b a" using ab unfolding symp_def by blast +qed + +lemma R_trans2: + assumes ac: "R a c" + and bd: "R b d" + shows "R a b = R c d" +using ac bd +by (blast intro: R_trans R_sym) + +lemma REPS_same: + shows "R (REP a) (REP b) \ (a = b)" +proof - + have "R (REP a) (REP b) = (a = b)" + proof + assume as: "R (REP a) (REP b)" + from rep_prop + obtain x y + where eqs: "Rep a = R x" "Rep b = R y" by blast + from eqs have "R (Eps (R x)) (Eps (R y))" using as unfolding REP_def by simp + then have "R x (Eps (R y))" using lem9 by simp + then have "R (Eps (R y)) x" using R_sym by blast + then have "R y x" using lem9 by simp + then have "R x y" using R_sym by blast + then have "ABS x = ABS y" using thm11 by simp + then have "Abs (Rep a) = Abs (Rep b)" using eqs unfolding ABS_def by simp + then show "a = b" using rep_inverse by simp + next + assume ab: "a = b" + have "reflp R" using equivp equivp_reflp_symp_transp[of R] by simp + then show "R (REP a) (REP b)" unfolding reflp_def using ab by auto + qed + then show "R (REP a) (REP b) \ (a = b)" by simp +qed + +end + +section {* type definition for the quotient type *} + +(* the auxiliary data for the quotient types *) +use "quotient_info.ML" + +declare [[map list = (map, list_rel)]] +declare [[map * = (prod_fun, prod_rel)]] +declare [[map "fun" = (fun_map, fun_rel)]] + +(* identity quotient is not here as it has to be applied first *) +lemmas [quotient_thm] = + fun_quotient list_quotient prod_quotient + +lemmas [quotient_rsp] = + quot_rel_rsp nil_rsp cons_rsp foldl_rsp pair_rsp + +(* fun_map is not here since equivp is not true *) +(* TODO: option, ... *) +lemmas [quotient_equiv] = + identity_equivp list_equivp prod_equivp + + +ML {* maps_lookup @{theory} "List.list" *} +ML {* maps_lookup @{theory} "*" *} +ML {* maps_lookup @{theory} "fun" *} + + +(* definition of the quotient types *) +(* FIXME: should be called quotient_typ.ML *) +use "quotient.ML" + + +(* lifting of constants *) +use "quotient_def.ML" + +section {* Simset setup *} + +(* since HOL_basic_ss is too "big", we need to set up *) +(* our own minimal simpset *) +ML {* +fun mk_minimal_ss ctxt = + Simplifier.context ctxt empty_ss + setsubgoaler asm_simp_tac + setmksimps (mksimps []) +*} + +section {* atomize *} + +lemma atomize_eqv[atomize]: + shows "(Trueprop A \ Trueprop B) \ (A \ B)" +proof + assume "A \ B" + then show "Trueprop A \ Trueprop B" by unfold +next + assume *: "Trueprop A \ Trueprop B" + have "A = B" + proof (cases A) + case True + have "A" by fact + then show "A = B" using * by simp + next + case False + have "\A" by fact + then show "A = B" using * by auto + qed + then show "A \ B" by (rule eq_reflection) +qed + +ML {* +fun atomize_thm thm = +let + val thm' = Thm.freezeT (forall_intr_vars thm) + val thm'' = ObjectLogic.atomize (cprop_of thm') +in + @{thm equal_elim_rule1} OF [thm'', thm'] +end +*} + +section {* infrastructure about id *} + +lemma prod_fun_id: "prod_fun id id \ id" + by (rule eq_reflection) (simp add: prod_fun_def) + +lemma map_id: "map id \ id" + apply (rule eq_reflection) + apply (rule ext) + apply (rule_tac list="x" in list.induct) + apply (simp_all) + done + +lemmas id_simps = + fun_map_id[THEN eq_reflection] + id_apply[THEN eq_reflection] + id_def[THEN eq_reflection,symmetric] + prod_fun_id map_id + +ML {* +fun simp_ids thm = + MetaSimplifier.rewrite_rule @{thms id_simps} thm +*} + +section {* Debugging infrastructure for testing tactics *} + +ML {* +fun my_print_tac ctxt s i thm = +let + val prem_str = nth (prems_of thm) (i - 1) + |> Syntax.string_of_term ctxt + handle Subscript => "no subgoal" + val _ = tracing (s ^ "\n" ^ prem_str) +in + Seq.single thm +end *} + +ML {* +fun DT ctxt s tac i thm = +let + val before_goal = nth (prems_of thm) (i - 1) + |> Syntax.string_of_term ctxt + val before_msg = ["before: " ^ s, before_goal, "after: " ^ s] + |> cat_lines +in + EVERY [tac i, my_print_tac ctxt before_msg i] thm +end + +fun NDT ctxt s tac thm = tac thm +*} + +section {* Matching of terms and types *} + +ML {* +fun matches_typ (ty, ty') = + case (ty, ty') of + (_, TVar _) => true + | (TFree x, TFree x') => x = x' + | (Type (s, tys), Type (s', tys')) => + s = s' andalso + if (length tys = length tys') + then (List.all matches_typ (tys ~~ tys')) + else false + | _ => false +*} + +ML {* +fun matches_term (trm, trm') = + case (trm, trm') of + (_, Var _) => true + | (Const (s, ty), Const (s', ty')) => s = s' andalso matches_typ (ty, ty') + | (Free (x, ty), Free (x', ty')) => x = x' andalso matches_typ (ty, ty') + | (Bound i, Bound j) => i = j + | (Abs (_, T, t), Abs (_, T', t')) => matches_typ (T, T') andalso matches_term (t, t') + | (t $ s, t' $ s') => matches_term (t, t') andalso matches_term (s, s') + | _ => false +*} + +section {* Infrastructure for collecting theorems for starting the lifting *} + +ML {* +fun lookup_quot_data lthy qty = + let + val qty_name = fst (dest_Type qty) + val SOME quotdata = quotdata_lookup lthy qty_name + (* TODO: Should no longer be needed *) + val rty = Logic.unvarifyT (#rtyp quotdata) + val rel = #rel quotdata + val rel_eqv = #equiv_thm quotdata + val rel_refl = @{thm equivp_reflp} OF [rel_eqv] + in + (rty, rel, rel_refl, rel_eqv) + end +*} + +ML {* +fun lookup_quot_thms lthy qty_name = + let + val thy = ProofContext.theory_of lthy; + val trans2 = PureThy.get_thm thy ("QUOT_TYPE_I_" ^ qty_name ^ ".R_trans2") + val reps_same = PureThy.get_thm thy ("QUOT_TYPE_I_" ^ qty_name ^ ".REPS_same") + val absrep = PureThy.get_thm thy ("QUOT_TYPE_I_" ^ qty_name ^ ".thm10") + val quot = PureThy.get_thm thy ("Quotient_" ^ qty_name) + in + (trans2, reps_same, absrep, quot) + end +*} + +section {* Regularization *} + +(* +Regularizing an rtrm means: + - quantifiers over a type that needs lifting are replaced by + bounded quantifiers, for example: + \x. P \ \x \ (Respects R). P / All (Respects R) P + + the relation R is given by the rty and qty; + + - abstractions over a type that needs lifting are replaced + by bounded abstractions: + \x. P \ Ball (Respects R) (\x. P) + + - equalities over the type being lifted are replaced by + corresponding relations: + A = B \ A \ B + + example with more complicated types of A, B: + A = B \ (op = \ op \) A B +*) + +ML {* +(* builds the relation that is the argument of respects *) +fun mk_resp_arg lthy (rty, qty) = +let + val thy = ProofContext.theory_of lthy +in + if rty = qty + then HOLogic.eq_const rty + else + case (rty, qty) of + (Type (s, tys), Type (s', tys')) => + if s = s' + then let + val SOME map_info = maps_lookup thy s + val args = map (mk_resp_arg lthy) (tys ~~ tys') + in + list_comb (Const (#relfun map_info, dummyT), args) + end + else let + val SOME qinfo = quotdata_lookup_thy thy s' + (* FIXME: check in this case that the rty and qty *) + (* FIXME: correspond to each other *) + val (s, _) = dest_Const (#rel qinfo) + (* FIXME: the relation should only be the string *) + (* FIXME: and the type needs to be calculated as below; *) + (* FIXME: maybe one should actually have a term *) + (* FIXME: and one needs to force it to have this type *) + in + Const (s, rty --> rty --> @{typ bool}) + end + | _ => HOLogic.eq_const dummyT + (* FIXME: check that the types correspond to each other? *) +end +*} + +ML {* +val mk_babs = Const (@{const_name Babs}, dummyT) +val mk_ball = Const (@{const_name Ball}, dummyT) +val mk_bex = Const (@{const_name Bex}, dummyT) +val mk_resp = Const (@{const_name Respects}, dummyT) +*} + +ML {* +(* - applies f to the subterm of an abstraction, *) +(* otherwise to the given term, *) +(* - used by regularize, therefore abstracted *) +(* variables do not have to be treated specially *) + +fun apply_subt f trm1 trm2 = + case (trm1, trm2) of + (Abs (x, T, t), Abs (x', T', t')) => Abs (x, T, f t t') + | _ => f trm1 trm2 + +(* the major type of All and Ex quantifiers *) +fun qnt_typ ty = domain_type (domain_type ty) +*} + +ML {* +(* produces a regularized version of rtm *) +(* - the result is still not completely typed *) +(* - does not need any special treatment of *) +(* bound variables *) + +fun regularize_trm lthy rtrm qtrm = + case (rtrm, qtrm) of + (Abs (x, ty, t), Abs (x', ty', t')) => + let + val subtrm = Abs(x, ty, regularize_trm lthy t t') + in + if ty = ty' + then subtrm + else mk_babs $ (mk_resp $ mk_resp_arg lthy (ty, ty')) $ subtrm + end + + | (Const (@{const_name "All"}, ty) $ t, Const (@{const_name "All"}, ty') $ t') => + let + val subtrm = apply_subt (regularize_trm lthy) t t' + in + if ty = ty' + then Const (@{const_name "All"}, ty) $ subtrm + else mk_ball $ (mk_resp $ mk_resp_arg lthy (qnt_typ ty, qnt_typ ty')) $ subtrm + end + + | (Const (@{const_name "Ex"}, ty) $ t, Const (@{const_name "Ex"}, ty') $ t') => + let + val subtrm = apply_subt (regularize_trm lthy) t t' + in + if ty = ty' + then Const (@{const_name "Ex"}, ty) $ subtrm + else mk_bex $ (mk_resp $ mk_resp_arg lthy (qnt_typ ty, qnt_typ ty')) $ subtrm + end + + | (* equalities need to be replaced by appropriate equivalence relations *) + (Const (@{const_name "op ="}, ty), Const (@{const_name "op ="}, ty')) => + if ty = ty' + then rtrm + else mk_resp_arg lthy (domain_type ty, domain_type ty') + + | (* in this case we check whether the given equivalence relation is correct *) + (rel, Const (@{const_name "op ="}, ty')) => + let + val exc = LIFT_MATCH "regularise (relation mismatch)" + val rel_ty = (fastype_of rel) handle TERM _ => raise exc + val rel' = mk_resp_arg lthy (domain_type rel_ty, domain_type ty') + in + if rel' = rel + then rtrm + else raise exc + end + | (_, Const (s, _)) => + let + fun same_name (Const (s, _)) (Const (s', _)) = (s = s') + | same_name _ _ = false + in + if same_name rtrm qtrm + then rtrm + else + let + fun exc1 s = LIFT_MATCH ("regularize (constant " ^ s ^ " not found)") + val exc2 = LIFT_MATCH ("regularize (constant mismatch)") + val thy = ProofContext.theory_of lthy + val rtrm' = (#rconst (qconsts_lookup thy s)) handle NotFound => raise (exc1 s) + in + if matches_term (rtrm, rtrm') + then rtrm + else raise exc2 + end + end + + | (t1 $ t2, t1' $ t2') => + (regularize_trm lthy t1 t1') $ (regularize_trm lthy t2 t2') + + | (Free (x, ty), Free (x', ty')) => + (* this case cannot arrise as we start with two fully atomized terms *) + raise (LIFT_MATCH "regularize (frees)") + + | (Bound i, Bound i') => + if i = i' + then rtrm + else raise (LIFT_MATCH "regularize (bounds mismatch)") + + | (rt, qt) => + raise (LIFT_MATCH "regularize (default)") +*} + +ML {* +fun equiv_tac ctxt = + REPEAT_ALL_NEW (FIRST' + [resolve_tac (equiv_rules_get ctxt)]) +*} + +ML {* +fun equiv_solver_tac ss = equiv_tac (Simplifier.the_context ss) +val equiv_solver = Simplifier.mk_solver' "Equivalence goal solver" equiv_solver_tac +*} + +ML {* +fun prep_trm thy (x, (T, t)) = + (cterm_of thy (Var (x, T)), cterm_of thy t) + +fun prep_ty thy (x, (S, ty)) = + (ctyp_of thy (TVar (x, S)), ctyp_of thy ty) +*} + +ML {* +fun matching_prs thy pat trm = +let + val univ = Unify.matchers thy [(pat, trm)] + val SOME (env, _) = Seq.pull univ + val tenv = Vartab.dest (Envir.term_env env) + val tyenv = Vartab.dest (Envir.type_env env) +in + (map (prep_ty thy) tyenv, map (prep_trm thy) tenv) +end +*} + +ML {* +fun calculate_instance ctxt thm redex R1 R2 = +let + val thy = ProofContext.theory_of ctxt + val goal = Const (@{const_name "equivp"}, dummyT) $ R2 + |> Syntax.check_term ctxt + |> HOLogic.mk_Trueprop + val eqv_prem = Goal.prove ctxt [] [] goal (fn {context,...} => equiv_tac context 1) + val thm = (@{thm eq_reflection} OF [thm OF [eqv_prem]]) + val R1c = cterm_of thy R1 + val thmi = Drule.instantiate' [] [SOME R1c] thm + val inst = matching_prs thy (term_of (Thm.lhs_of thmi)) redex + val thm2 = Drule.eta_contraction_rule (Drule.instantiate inst thmi) +in + SOME thm2 +end +handle _ => NONE +(* FIXME/TODO: what is the place where the exception can be raised: matching_prs? *) +*} + +ML {* +fun ball_bex_range_simproc ss redex = +let + val ctxt = Simplifier.the_context ss +in + case redex of + (Const (@{const_name "Ball"}, _) $ (Const (@{const_name "Respects"}, _) $ + (Const (@{const_name "fun_rel"}, _) $ R1 $ R2)) $ _) => + calculate_instance ctxt @{thm ball_reg_eqv_range} redex R1 R2 + | (Const (@{const_name "Bex"}, _) $ (Const (@{const_name "Respects"}, _) $ + (Const (@{const_name "fun_rel"}, _) $ R1 $ R2)) $ _) => + calculate_instance ctxt @{thm bex_reg_eqv_range} redex R1 R2 + | _ => NONE +end +*} + +lemma eq_imp_rel: + shows "equivp R \ a = b \ R a b" +by (simp add: equivp_reflp) + +(* FIXME/TODO: How does regularizing work? *) +(* FIXME/TODO: needs to be adapted + +To prove that the raw theorem implies the regularised one, +we try in order: + + - Reflexivity of the relation + - Assumption + - Elimnating quantifiers on both sides of toplevel implication + - Simplifying implications on both sides of toplevel implication + - Ball (Respects ?E) ?P = All ?P + - (\x. ?R x \ ?P x \ ?Q x) \ All ?P \ Ball ?R ?Q + +*) +ML {* +fun regularize_tac ctxt = +let + val thy = ProofContext.theory_of ctxt + val pat_ball = @{term "Ball (Respects (R1 ===> R2)) P"} + val pat_bex = @{term "Bex (Respects (R1 ===> R2)) P"} + val simproc = Simplifier.simproc_i thy "" [pat_ball, pat_bex] (K (ball_bex_range_simproc)) + val simpset = (mk_minimal_ss ctxt) + addsimps @{thms ball_reg_eqv bex_reg_eqv} + addsimprocs [simproc] addSolver equiv_solver + (* TODO: Make sure that there are no list_rel, pair_rel etc involved *) + val eq_eqvs = map (fn x => @{thm eq_imp_rel} OF [x]) (equiv_rules_get ctxt) +in + ObjectLogic.full_atomize_tac THEN' + simp_tac simpset THEN' + REPEAT_ALL_NEW (FIRST' [ + rtac @{thm ball_reg_right}, + rtac @{thm bex_reg_left}, + resolve_tac (Inductive.get_monos ctxt), + rtac @{thm ball_all_comm}, + rtac @{thm bex_ex_comm}, + resolve_tac eq_eqvs, + simp_tac simpset]) +end +*} + +section {* Injections of rep and abses *} + +(* +Injecting repabs means: + + For abstractions: + * If the type of the abstraction doesn't need lifting we recurse. + * If it does we add RepAbs around the whole term and check if the + variable needs lifting. + * If it doesn't then we recurse + * If it does we recurse and put 'RepAbs' around all occurences + of the variable in the obtained subterm. This in combination + with the RepAbs above will let us change the type of the + abstraction with rewriting. + For applications: + * If the term is 'Respects' applied to anything we leave it unchanged + * If the term needs lifting and the head is a constant that we know + how to lift, we put a RepAbs and recurse + * If the term needs lifting and the head is a free applied to subterms + (if it is not applied we treated it in Abs branch) then we + put RepAbs and recurse + * Otherwise just recurse. +*) + +ML {* +fun mk_repabs lthy (T, T') trm = + Quotient_Def.get_fun repF lthy (T, T') + $ (Quotient_Def.get_fun absF lthy (T, T') $ trm) +*} + +ML {* +(* bound variables need to be treated properly, *) +(* as the type of subterms need to be calculated *) +(* in the abstraction case *) + +fun inj_repabs_trm lthy (rtrm, qtrm) = + case (rtrm, qtrm) of + (Const (@{const_name "Ball"}, T) $ r $ t, Const (@{const_name "All"}, _) $ t') => + Const (@{const_name "Ball"}, T) $ r $ (inj_repabs_trm lthy (t, t')) + + | (Const (@{const_name "Bex"}, T) $ r $ t, Const (@{const_name "Ex"}, _) $ t') => + Const (@{const_name "Bex"}, T) $ r $ (inj_repabs_trm lthy (t, t')) + + | (Const (@{const_name "Babs"}, T) $ r $ t, t' as (Abs _)) => + Const (@{const_name "Babs"}, T) $ r $ (inj_repabs_trm lthy (t, t')) + + | (Abs (x, T, t), Abs (x', T', t')) => + let + val rty = fastype_of rtrm + val qty = fastype_of qtrm + val (y, s) = Term.dest_abs (x, T, t) + val (_, s') = Term.dest_abs (x', T', t') + val yvar = Free (y, T) + val result = Term.lambda_name (y, yvar) (inj_repabs_trm lthy (s, s')) + in + if rty = qty + then result + else mk_repabs lthy (rty, qty) result + end + + | (t $ s, t' $ s') => + (inj_repabs_trm lthy (t, t')) $ (inj_repabs_trm lthy (s, s')) + + | (Free (_, T), Free (_, T')) => + if T = T' + then rtrm + else mk_repabs lthy (T, T') rtrm + + | (_, Const (@{const_name "op ="}, _)) => rtrm + + (* FIXME: check here that rtrm is the corresponding definition for the const *) + | (_, Const (_, T')) => + let + val rty = fastype_of rtrm + in + if rty = T' + then rtrm + else mk_repabs lthy (rty, T') rtrm + end + + | _ => raise (LIFT_MATCH "injection") +*} + +section {* RepAbs Injection Tactic *} + +ML {* +fun quotient_tac ctxt = + REPEAT_ALL_NEW (FIRST' + [rtac @{thm identity_quotient}, + resolve_tac (quotient_rules_get ctxt)]) +*} + +(* solver for the simplifier *) +ML {* +fun quotient_solver_tac ss = quotient_tac (Simplifier.the_context ss) +val quotient_solver = Simplifier.mk_solver' "Quotient goal solver" quotient_solver_tac +*} + +ML {* +fun solve_quotient_assums ctxt thm = + let val gl = hd (Drule.strip_imp_prems (cprop_of thm)) in + thm OF [Goal.prove_internal [] gl (fn _ => quotient_tac ctxt 1)] + end + handle _ => error "solve_quotient_assums failed. Maybe a quotient_thm is missing" +*} + +(* Not used *) +(* It proves the Quotient assumptions by calling quotient_tac *) +ML {* +fun solve_quotient_assum i ctxt thm = + let + val tac = + (compose_tac (false, thm, i)) THEN_ALL_NEW + (quotient_tac ctxt); + val gc = Drule.strip_imp_concl (cprop_of thm); + in + Goal.prove_internal [] gc (fn _ => tac 1) + end + handle _ => error "solve_quotient_assum" +*} + +definition + "QUOT_TRUE x \ True" + +ML {* +fun find_qt_asm asms = + let + fun find_fun trm = + case trm of + (Const(@{const_name Trueprop}, _) $ (Const (@{const_name QUOT_TRUE}, _) $ _)) => true + | _ => false + in + case find_first find_fun asms of + SOME (_ $ (_ $ (f $ a))) => (f, a) + | SOME _ => error "find_qt_asm: no pair" + | NONE => error "find_qt_asm: no assumption" + end +*} + +(* +To prove that the regularised theorem implies the abs/rep injected, +we try: + + 1) theorems 'trans2' from the appropriate QUOT_TYPE + 2) remove lambdas from both sides: lambda_rsp_tac + 3) remove Ball/Bex from the right hand side + 4) use user-supplied RSP theorems + 5) remove rep_abs from the right side + 6) reflexivity of equality + 7) split applications of lifted type (apply_rsp) + 8) split applications of non-lifted type (cong_tac) + 9) apply extentionality + A) reflexivity of the relation + B) assumption + (Lambdas under respects may have left us some assumptions) + C) proving obvious higher order equalities by simplifying fun_rel + (not sure if it is still needed?) + D) unfolding lambda on one side + E) simplifying (= ===> =) for simpler respectfulness + +*) + +lemma quot_true_dests: + shows QT_all: "QUOT_TRUE (All P) \ QUOT_TRUE P" + and QT_ex: "QUOT_TRUE (Ex P) \ QUOT_TRUE P" + and QT_lam: "QUOT_TRUE (\x. P x) \ (\x. QUOT_TRUE (P x))" + and QT_ext: "(\x. QUOT_TRUE (a x) \ f x = g x) \ (QUOT_TRUE a \ f = g)" +apply(simp_all add: QUOT_TRUE_def ext) +done + +lemma QUOT_TRUE_i: "(QUOT_TRUE (a :: bool) \ P) \ P" +by (simp add: QUOT_TRUE_def) + +lemma QUOT_TRUE_imp: "QUOT_TRUE a \ QUOT_TRUE b" +by (simp add: QUOT_TRUE_def) + +ML {* +fun quot_true_conv1 ctxt fnctn ctrm = + case (term_of ctrm) of + (Const (@{const_name QUOT_TRUE}, _) $ x) => + let + val fx = fnctn x; + val thy = ProofContext.theory_of ctxt; + val cx = cterm_of thy x; + val cfx = cterm_of thy fx; + val cxt = ctyp_of thy (fastype_of x); + val cfxt = ctyp_of thy (fastype_of fx); + val thm = Drule.instantiate' [SOME cxt, SOME cfxt] [SOME cx, SOME cfx] @{thm QUOT_TRUE_imp} + in + Conv.rewr_conv thm ctrm + end +*} + +ML {* +fun quot_true_conv ctxt fnctn ctrm = + case (term_of ctrm) of + (Const (@{const_name QUOT_TRUE}, _) $ _) => + quot_true_conv1 ctxt fnctn ctrm + | _ $ _ => Conv.comb_conv (quot_true_conv ctxt fnctn) ctrm + | Abs _ => Conv.abs_conv (fn (_, ctxt) => quot_true_conv ctxt fnctn) ctxt ctrm + | _ => Conv.all_conv ctrm +*} + +ML {* +fun quot_true_tac ctxt fnctn = CONVERSION + ((Conv.params_conv ~1 (fn ctxt => + (Conv.prems_conv ~1 (quot_true_conv ctxt fnctn)))) ctxt) +*} + +ML {* fun dest_comb (f $ a) = (f, a) *} +ML {* fun dest_bcomb ((_ $ l) $ r) = (l, r) *} +(* TODO: Can this be done easier? *) +ML {* +fun unlam t = + case t of + (Abs a) => snd (Term.dest_abs a) + | _ => unlam (Abs("", domain_type (fastype_of t), (incr_boundvars 1 t) $ (Bound 0))) +*} + +ML {* +fun dest_fun_type (Type("fun", [T, S])) = (T, S) + | dest_fun_type _ = error "dest_fun_type" +*} + +ML {* +val bare_concl = HOLogic.dest_Trueprop o Logic.strip_assums_concl +*} + +ML {* +val apply_rsp_tac = + Subgoal.FOCUS (fn {concl, asms, context,...} => + case ((HOLogic.dest_Trueprop (term_of concl))) of + ((R2 $ (f $ x) $ (g $ y))) => + (let + val (asmf, asma) = find_qt_asm (map term_of asms); + in + if (fastype_of asmf) = (fastype_of f) then no_tac else let + val ty_a = fastype_of x; + val ty_b = fastype_of asma; + val ty_c = range_type (type_of f); + val thy = ProofContext.theory_of context; + val ty_inst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c]; + val thm = Drule.instantiate' ty_inst [] @{thm apply_rsp} + val te = solve_quotient_assums context thm + val t_inst = map (SOME o (cterm_of thy)) [R2, f, g, x, y]; + val thm = Drule.instantiate' [] t_inst te + in + compose_tac (false, thm, 2) 1 + end + end + handle ERROR "find_qt_asm: no pair" => no_tac) + | _ => no_tac) +*} +ML {* +fun SOLVES' tac = tac THEN_ALL_NEW (fn _ => no_tac) +*} + +ML {* +fun rep_abs_rsp_tac ctxt = + SUBGOAL (fn (goal, i) => + case (bare_concl goal) of + (rel $ _ $ (rep $ (abs $ _))) => + (let + val thy = ProofContext.theory_of ctxt; + val (ty_a, ty_b) = dest_fun_type (fastype_of abs); + val ty_inst = map (SOME o (ctyp_of thy)) [ty_a, ty_b]; + val t_inst = map (SOME o (cterm_of thy)) [rel, abs, rep]; + val thm = Drule.instantiate' ty_inst t_inst @{thm rep_abs_rsp} + val te = solve_quotient_assums ctxt thm + in + rtac te i + end + handle _ => no_tac) + | _ => no_tac) +*} + +ML {* +fun inj_repabs_tac_match ctxt trans2 = SUBGOAL (fn (goal, i) => +(case (bare_concl goal) of + (* (R1 ===> R2) (\x\) (\y\) ----> \R1 x y\ \ R2 (\x) (\y) *) + ((Const (@{const_name fun_rel}, _) $ _ $ _) $ (Abs _) $ (Abs _)) + => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam + + (* (op =) (Ball\) (Ball\) ----> (op =) (\) (\) *) +| (Const (@{const_name "op ="},_) $ + (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ + (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _)) + => rtac @{thm ball_rsp} THEN' dtac @{thm QT_all} + + (* (R1 ===> op =) (Ball\) (Ball\) ----> \R1 x y\ \ (Ball\x) = (Ball\y) *) +| (Const (@{const_name fun_rel}, _) $ _ $ _) $ + (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ + (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) + => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam + + (* (op =) (Bex\) (Bex\) ----> (op =) (\) (\) *) +| Const (@{const_name "op ="},_) $ + (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ + (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) + => rtac @{thm bex_rsp} THEN' dtac @{thm QT_ex} + + (* (R1 ===> op =) (Bex\) (Bex\) ----> \R1 x y\ \ (Bex\x) = (Bex\y) *) +| (Const (@{const_name fun_rel}, _) $ _ $ _) $ + (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ + (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) + => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam + +| (_ $ + (Const(@{const_name Babs},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ + (Const(@{const_name Babs},_) $ (Const (@{const_name Respects}, _) $ _) $ _)) + => rtac @{thm babs_rsp} THEN' RANGE [quotient_tac ctxt] + + (* reflexivity of operators arising from Cong_tac *) +| Const (@{const_name "op ="},_) $ _ $ _ + => rtac @{thm refl} ORELSE' + (resolve_tac trans2 THEN' RANGE [ + quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)]) + +(* TODO: These patterns should should be somehow combined and generalized... *) +| (Const (@{const_name fun_rel}, _) $ _ $ _) $ + (Const (@{const_name fun_rel}, _) $ _ $ _) $ + (Const (@{const_name fun_rel}, _) $ _ $ _) + => rtac @{thm quot_rel_rsp} THEN_ALL_NEW quotient_tac ctxt + +| (Const (@{const_name fun_rel}, _) $ _ $ _) $ + (Const (@{const_name prod_rel}, _) $ _ $ _) $ + (Const (@{const_name prod_rel}, _) $ _ $ _) + => rtac @{thm quot_rel_rsp} THEN_ALL_NEW quotient_tac ctxt + + (* respectfulness of constants; in particular of a simple relation *) +| _ $ (Const _) $ (Const _) (* fun_rel, list_rel, etc but not equality *) + => resolve_tac (rsp_rules_get ctxt) THEN_ALL_NEW quotient_tac ctxt + + (* R (\) (Rep (Abs \)) ----> R (\) (\) *) + (* observe ---> *) +| _ $ _ $ _ + => rep_abs_rsp_tac ctxt + +| _ => error "inj_repabs_tac not a relation" +) i) +*} + +ML {* +fun inj_repabs_tac ctxt rel_refl trans2 = + (FIRST' [ + inj_repabs_tac_match ctxt trans2, + (* R (t $ \) (t' $ \) ----> apply_rsp provided type of t needs lifting *) + NDT ctxt "A" (apply_rsp_tac ctxt THEN' + (RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)])), + (* (op =) (t $ \) (t' $ \) ----> Cong provided type of t does not need lifting *) + (* merge with previous tactic *) + NDT ctxt "B" (Cong_Tac.cong_tac @{thm cong} THEN' + (RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)])), + (* (op =) (\x\) (\x\) ----> (op =) (\) (\) *) + NDT ctxt "C" (rtac @{thm ext} THEN' quot_true_tac ctxt unlam), + (* resolving with R x y assumptions *) + NDT ctxt "E" (atac), + (* reflexivity of the basic relations *) + (* R \ \ *) + NDT ctxt "D" (resolve_tac rel_refl) + ]) +*} + +ML {* +fun all_inj_repabs_tac ctxt rel_refl trans2 = + REPEAT_ALL_NEW (inj_repabs_tac ctxt rel_refl trans2) +*} + +section {* Cleaning of the theorem *} + +ML {* +fun make_inst lhs t = + let + val _ $ (Abs (_, _, (f as Var (_, Type ("fun", [T, _]))) $ u)) = lhs; + val _ $ (Abs (_, _, g)) = t; + fun mk_abs i t = + if incr_boundvars i u aconv t then Bound i + else (case t of + t1 $ t2 => mk_abs i t1 $ mk_abs i t2 + | Abs (s, T, t') => Abs (s, T, mk_abs (i + 1) t') + | Bound j => if i = j then error "make_inst" else t + | _ => t); + in (f, Abs ("x", T, mk_abs 0 g)) end; +*} + +ML {* +fun lambda_prs_simple_conv ctxt ctrm = + case (term_of ctrm) of + ((Const (@{const_name fun_map}, _) $ r1 $ (a2 as (Const (s,_)))) $ (Abs _)) => + let + val thy = ProofContext.theory_of ctxt + val (ty_b, ty_a) = dest_fun_type (fastype_of r1) + val (ty_c, ty_d) = dest_fun_type (fastype_of a2) + val tyinst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c, ty_d] + val tinst = [NONE, NONE, SOME (cterm_of thy r1), NONE, SOME (cterm_of thy a2)] + val lpi = Drule.instantiate' tyinst tinst @{thm lambda_prs} + val te = @{thm eq_reflection} OF [solve_quotient_assums ctxt (solve_quotient_assums ctxt lpi)] + val ts = MetaSimplifier.rewrite_rule @{thms id_simps} te + val _ = tracing ("te rule:\n" ^ (Syntax.string_of_term ctxt (prop_of te))); + val tl = Thm.lhs_of ts + val (insp, inst) = make_inst (term_of tl) (term_of ctrm) + val ti = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts + val _ = if not (s = @{const_name "id"}) then + (tracing "lambda_prs"; + tracing ("redex:\n" ^ (Syntax.string_of_term ctxt (term_of ctrm))); + tracing ("lpi rule:\n" ^ (Syntax.string_of_term ctxt (prop_of lpi))); + tracing ("te rule:\n" ^ (Syntax.string_of_term ctxt (prop_of te))); + tracing ("ts rule:\n" ^ (Syntax.string_of_term ctxt (prop_of ts))); + tracing ("instantiated rule:\n" ^ (Syntax.string_of_term ctxt (prop_of ti)))) + else () + in + Conv.rewr_conv ti ctrm + end + | _ => Conv.all_conv ctrm +*} + +ML {* +val lambda_prs_conv = + More_Conv.top_conv lambda_prs_simple_conv + +fun lambda_prs_tac ctxt = CONVERSION (lambda_prs_conv ctxt) +*} + +(* + Cleaning the theorem consists of three rewriting steps. + The first two need to be done before fun_map is unfolded + + 1) lambda_prs: + (Rep1 ---> Abs2) (\x. Rep2 (f (Abs1 x))) ----> f + + Implemented as conversion since it is not a pattern. + + 2) all_prs (the same for exists): + Ball (Respects R) ((abs ---> id) f) ----> All f + + Rewriting with definitions from the argument defs + (rep ---> abs) oldConst ----> newconst + + 3) Quotient_rel_rep: + Rel (Rep x) (Rep y) ----> x = y + + Quotient_abs_rep: + Abs (Rep x) ----> x + + id_simps; fun_map.simps +*) + +ML {* +fun clean_tac lthy = + let + val thy = ProofContext.theory_of lthy; + val defs = map (Thm.varifyT o symmetric o #def) (qconsts_dest thy) + (* FIXME: shouldn't the definitions already be varified? *) + val thms1 = @{thms all_prs ex_prs} @ defs + val thms2 = @{thms eq_reflection[OF fun_map.simps]} + @ @{thms id_simps Quotient_abs_rep Quotient_rel_rep} + fun simps thms = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver + in + EVERY' [lambda_prs_tac lthy, + simp_tac (simps thms1), + simp_tac (simps thms2), + TRY o rtac refl] + end +*} + +section {* Genralisation of free variables in a goal *} + +ML {* +fun inst_spec ctrm = + Drule.instantiate' [SOME (ctyp_of_term ctrm)] [NONE, SOME ctrm] @{thm spec} + +fun inst_spec_tac ctrms = + EVERY' (map (dtac o inst_spec) ctrms) + +fun all_list xs trm = + fold (fn (x, T) => fn t' => HOLogic.mk_all (x, T, t')) xs trm + +fun apply_under_Trueprop f = + HOLogic.dest_Trueprop #> f #> HOLogic.mk_Trueprop + +fun gen_frees_tac ctxt = + SUBGOAL (fn (concl, i) => + let + val thy = ProofContext.theory_of ctxt + val vrs = Term.add_frees concl [] + val cvrs = map (cterm_of thy o Free) vrs + val concl' = apply_under_Trueprop (all_list vrs) concl + val goal = Logic.mk_implies (concl', concl) + val rule = Goal.prove ctxt [] [] goal + (K (EVERY1 [inst_spec_tac (rev cvrs), atac])) + in + rtac rule i + end) +*} + +section {* General outline of the lifting procedure *} + +(* - A is the original raw theorem *) +(* - B is the regularized theorem *) +(* - C is the rep/abs injected version of B *) +(* - D is the lifted theorem *) +(* *) +(* - b is the regularization step *) +(* - c is the rep/abs injection step *) +(* - d is the cleaning part *) + +lemma lifting_procedure: + assumes a: "A" + and b: "A \ B" + and c: "B = C" + and d: "C = D" + shows "D" + using a b c d + by simp + +ML {* +fun lift_match_error ctxt fun_str rtrm qtrm = +let + val rtrm_str = Syntax.string_of_term ctxt rtrm + val qtrm_str = Syntax.string_of_term ctxt qtrm + val msg = [enclose "[" "]" fun_str, "The quotient theorem\n", qtrm_str, + "and the lifted theorem\n", rtrm_str, "do not match"] +in + error (space_implode " " msg) +end +*} + +ML {* +fun procedure_inst ctxt rtrm qtrm = +let + val thy = ProofContext.theory_of ctxt + val rtrm' = HOLogic.dest_Trueprop rtrm + val qtrm' = HOLogic.dest_Trueprop qtrm + val reg_goal = + Syntax.check_term ctxt (regularize_trm ctxt rtrm' qtrm') + handle (LIFT_MATCH s) => lift_match_error ctxt s rtrm qtrm + val _ = warning "Regularization done." + val inj_goal = + Syntax.check_term ctxt (inj_repabs_trm ctxt (reg_goal, qtrm')) + handle (LIFT_MATCH s) => lift_match_error ctxt s rtrm qtrm + val _ = warning "RepAbs Injection done." +in + Drule.instantiate' [] + [SOME (cterm_of thy rtrm'), + SOME (cterm_of thy reg_goal), + SOME (cterm_of thy inj_goal)] @{thm lifting_procedure} +end +*} + +(* Left for debugging *) +ML {* +fun procedure_tac ctxt rthm = + ObjectLogic.full_atomize_tac + THEN' gen_frees_tac ctxt + THEN' CSUBGOAL (fn (gl, i) => + let + val rthm' = atomize_thm rthm + val rule = procedure_inst ctxt (prop_of rthm') (term_of gl) + val thm = Drule.instantiate' [] [SOME (snd (Thm.dest_comb gl))] @{thm QUOT_TRUE_i} + in + (rtac rule THEN' RANGE [rtac rthm', (fn _ => all_tac), rtac thm]) i + end) +*} + +ML {* +(* FIXME/TODO should only get as arguments the rthm like procedure_tac *) + +fun lift_tac ctxt rthm = + ObjectLogic.full_atomize_tac + THEN' gen_frees_tac ctxt + THEN' CSUBGOAL (fn (gl, i) => + let + val rthm' = atomize_thm rthm + val rule = procedure_inst ctxt (prop_of rthm') (term_of gl) + val rel_refl = map (fn x => @{thm equivp_reflp} OF [x]) (equiv_rules_get ctxt) + val quotients = quotient_rules_get ctxt + val trans2 = map (fn x => @{thm equals_rsp} OF [x]) quotients + val thm = Drule.instantiate' [] [SOME (snd (Thm.dest_comb gl))] @{thm QUOT_TRUE_i} + in + (rtac rule THEN' + RANGE [rtac rthm', + regularize_tac ctxt, + rtac thm THEN' all_inj_repabs_tac ctxt rel_refl trans2, + clean_tac ctxt]) i + end) +*} + +end + diff -r 6088fea1c8b1 -r 8a1c8dc72b5c Quot/QuotProd.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Quot/QuotProd.thy Mon Dec 07 14:09:50 2009 +0100 @@ -0,0 +1,80 @@ +theory QuotProd +imports QuotScript +begin + +fun + prod_rel +where + "prod_rel r1 r2 = (\(a,b) (c,d). r1 a c \ r2 b d)" + +(* prod_fun is a good mapping function *) + +lemma prod_equivp: + assumes a: "equivp R1" + assumes b: "equivp R2" + shows "equivp (prod_rel R1 R2)" +unfolding equivp_reflp_symp_transp reflp_def symp_def transp_def +apply(auto simp add: equivp_reflp[OF a] equivp_reflp[OF b]) +apply(simp only: equivp_symp[OF a]) +apply(simp only: equivp_symp[OF b]) +using equivp_transp[OF a] apply blast +using equivp_transp[OF b] apply blast +done + +lemma prod_quotient: + assumes q1: "Quotient R1 Abs1 Rep1" + assumes q2: "Quotient R2 Abs2 Rep2" + shows "Quotient (prod_rel R1 R2) (prod_fun Abs1 Abs2) (prod_fun Rep1 Rep2)" +unfolding Quotient_def +apply (simp add: Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2] Quotient_rel_rep[OF q1] Quotient_rel_rep[OF q2]) +using Quotient_rel[OF q1] Quotient_rel[OF q2] by blast + +lemma pair_rsp: + assumes q1: "Quotient R1 Abs1 Rep1" + assumes q2: "Quotient R2 Abs2 Rep2" + shows "(R1 ===> R2 ===> prod_rel R1 R2) Pair Pair" +by auto + +lemma pair_prs: + assumes q1: "Quotient R1 Abs1 Rep1" + assumes q2: "Quotient R2 Abs2 Rep2" + shows "(prod_fun Abs1 Abs2) (Rep1 l, Rep2 r) \ (l, r)" + by (simp add: Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]) + +(* TODO: Is the quotient assumption q1 necessary? *) +(* TODO: Aren't there hard to use later? *) +lemma fst_rsp: + assumes q1: "Quotient R1 Abs1 Rep1" + assumes q2: "Quotient R2 Abs2 Rep2" + assumes a: "(prod_rel R1 R2) p1 p2" + shows "R1 (fst p1) (fst p2)" + using a + apply(case_tac p1) + apply(case_tac p2) + apply(auto) + done + +lemma snd_rsp: + assumes q1: "Quotient R1 Abs1 Rep1" + assumes q2: "Quotient R2 Abs2 Rep2" + assumes a: "(prod_rel R1 R2) p1 p2" + shows "R2 (snd p1) (snd p2)" + using a + apply(case_tac p1) + apply(case_tac p2) + apply(auto) + done + +lemma fst_prs: + assumes q1: "Quotient R1 Abs1 Rep1" + assumes q2: "Quotient R2 Abs2 Rep2" + shows "Abs1 (fst ((prod_fun Rep1 Rep2) p)) = fst p" +by (case_tac p) (auto simp add: Quotient_abs_rep[OF q1]) + +lemma snd_prs: + assumes q1: "Quotient R1 Abs1 Rep1" + assumes q2: "Quotient R2 Abs2 Rep2" + shows "Abs2 (snd ((prod_fun Rep1 Rep2) p)) = snd p" +by (case_tac p) (auto simp add: Quotient_abs_rep[OF q2]) + +end diff -r 6088fea1c8b1 -r 8a1c8dc72b5c Quot/QuotScript.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Quot/QuotScript.thy Mon Dec 07 14:09:50 2009 +0100 @@ -0,0 +1,569 @@ +theory QuotScript +imports Plain ATP_Linkup +begin + +definition + "equivp E \ \x y. E x y = (E x = E y)" + +definition + "reflp E \ \x. E x x" + +definition + "symp E \ \x y. E x y \ E y x" + +definition + "transp E \ \x y z. E x y \ E y z \ E x z" + +lemma equivp_reflp_symp_transp: + shows "equivp E = (reflp E \ symp E \ transp E)" + unfolding equivp_def reflp_def symp_def transp_def expand_fun_eq + by (blast) + +lemma equivp_reflp: + shows "equivp E \ (\x. E x x)" + by (simp only: equivp_reflp_symp_transp reflp_def) + +lemma equivp_symp: + shows "equivp E \ (\x y. E x y \ E y x)" + by (metis equivp_reflp_symp_transp symp_def) + +lemma equivp_transp: + shows "equivp E \ (\x y z. E x y \ E y z \ E x z)" +by (metis equivp_reflp_symp_transp transp_def) + +definition + "part_equivp E \ (\x. E x x) \ (\x y. E x y = (E x x \ E y y \ (E x = E y)))" + +lemma equivp_IMP_part_equivp: + assumes a: "equivp E" + shows "part_equivp E" + using a unfolding equivp_def part_equivp_def + by auto + +definition + "Quotient E Abs Rep \ (\a. Abs (Rep a) = a) \ + (\a. E (Rep a) (Rep a)) \ + (\r s. E r s = (E r r \ E s s \ (Abs r = Abs s)))" + +lemma Quotient_abs_rep: + assumes a: "Quotient E Abs Rep" + shows "Abs (Rep a) \ a" + using a unfolding Quotient_def + by simp + +lemma Quotient_rep_reflp: + assumes a: "Quotient E Abs Rep" + shows "E (Rep a) (Rep a)" + using a unfolding Quotient_def + by blast + +lemma Quotient_rel: + assumes a: "Quotient E Abs Rep" + shows " E r s = (E r r \ E s s \ (Abs r = Abs s))" + using a unfolding Quotient_def + by blast + +lemma Quotient_rel_rep: + assumes a: "Quotient R Abs Rep" + shows "R (Rep a) (Rep b) \ (a = b)" + apply (rule eq_reflection) + using a unfolding Quotient_def + by metis + +lemma Quotient_rep_abs: + assumes a: "Quotient R Abs Rep" + shows "R r r \ R (Rep (Abs r)) r" + using a unfolding Quotient_def + by blast + +lemma identity_equivp: + shows "equivp (op =)" + unfolding equivp_def + by auto + +lemma identity_quotient: + shows "Quotient (op =) id id" + unfolding Quotient_def id_def + by blast + +lemma Quotient_symp: + assumes a: "Quotient E Abs Rep" + shows "symp E" + using a unfolding Quotient_def symp_def + by metis + +lemma Quotient_transp: + assumes a: "Quotient E Abs Rep" + shows "transp E" + using a unfolding Quotient_def transp_def + by metis + +fun + fun_map +where + "fun_map f g h x = g (h (f x))" + +abbreviation + fun_map_syn (infixr "--->" 55) +where + "f ---> g \ fun_map f g" + +lemma fun_map_id: + shows "(id ---> id) = id" + by (simp add: expand_fun_eq id_def) + +fun + fun_rel +where + "fun_rel E1 E2 f g = (\x y. E1 x y \ E2 (f x) (g y))" + +abbreviation + fun_rel_syn (infixr "===>" 55) +where + "E1 ===> E2 \ fun_rel E1 E2" + +lemma fun_rel_eq: + "(op =) ===> (op =) \ (op =)" +by (rule eq_reflection) (simp add: expand_fun_eq) + +lemma fun_quotient: + assumes q1: "Quotient R1 abs1 rep1" + and q2: "Quotient R2 abs2 rep2" + shows "Quotient (R1 ===> R2) (rep1 ---> abs2) (abs1 ---> rep2)" +proof - + have "\a. (rep1 ---> abs2) ((abs1 ---> rep2) a) = a" + apply(simp add: expand_fun_eq) + using q1 q2 + apply(simp add: Quotient_def) + done + moreover + have "\a. (R1 ===> R2) ((abs1 ---> rep2) a) ((abs1 ---> rep2) a)" + apply(auto) + using q1 q2 unfolding Quotient_def + apply(metis) + done + moreover + have "\r s. (R1 ===> R2) r s = ((R1 ===> R2) r r \ (R1 ===> R2) s s \ + (rep1 ---> abs2) r = (rep1 ---> abs2) s)" + apply(auto simp add: expand_fun_eq) + using q1 q2 unfolding Quotient_def + apply(metis) + using q1 q2 unfolding Quotient_def + apply(metis) + using q1 q2 unfolding Quotient_def + apply(metis) + using q1 q2 unfolding Quotient_def + apply(metis) + done + ultimately + show "Quotient (R1 ===> R2) (rep1 ---> abs2) (abs1 ---> rep2)" + unfolding Quotient_def by blast +qed + +definition + Respects +where + "Respects R x \ (R x x)" + +lemma in_respects: + shows "(x \ Respects R) = R x x" + unfolding mem_def Respects_def by simp + +lemma equals_rsp: + assumes q: "Quotient R Abs Rep" + and a: "R xa xb" "R ya yb" + shows "R xa ya = R xb yb" + using Quotient_symp[OF q] Quotient_transp[OF q] unfolding symp_def transp_def + using a by blast + +lemma lambda_prs: + assumes q1: "Quotient R1 Abs1 Rep1" + and q2: "Quotient R2 Abs2 Rep2" + shows "(Rep1 ---> Abs2) (\x. Rep2 (f (Abs1 x))) = (\x. f x)" + unfolding expand_fun_eq + using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2] + by simp + +lemma lambda_prs1: + assumes q1: "Quotient R1 Abs1 Rep1" + and q2: "Quotient R2 Abs2 Rep2" + shows "(Rep1 ---> Abs2) (\x. (Abs1 ---> Rep2) f x) = (\x. f x)" + unfolding expand_fun_eq + using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2] + by simp + +lemma rep_abs_rsp: + assumes q: "Quotient R Abs Rep" + and a: "R x1 x2" + shows "R x1 (Rep (Abs x2))" + using q a by (metis Quotient_rel[OF q] Quotient_abs_rep[OF q] Quotient_rep_reflp[OF q]) + +(* In the following theorem R1 can be instantiated with anything, + but we know some of the types of the Rep and Abs functions; + so by solving Quotient assumptions we can get a unique R1 that + will be provable; which is why we need to use apply_rsp and + not the primed version *) +lemma apply_rsp: + assumes q: "Quotient R1 Abs1 Rep1" + and a: "(R1 ===> R2) f g" "R1 x y" + shows "R2 ((f::'a\'c) x) ((g::'a\'c) y)" + using a by simp + +lemma apply_rsp': + assumes a: "(R1 ===> R2) f g" "R1 x y" + shows "R2 (f x) (g y)" + using a by simp + +(* Set of lemmas for regularisation of ball and bex *) + +lemma ball_reg_eqv: + fixes P :: "'a \ bool" + assumes a: "equivp R" + shows "Ball (Respects R) P = (All P)" + by (metis equivp_def in_respects a) + +lemma bex_reg_eqv: + fixes P :: "'a \ bool" + assumes a: "equivp R" + shows "Bex (Respects R) P = (Ex P)" + by (metis equivp_def in_respects a) + +lemma ball_reg_right: + assumes a: "\x. R x \ P x \ Q x" + shows "All P \ Ball R Q" + by (metis COMBC_def Collect_def Collect_mem_eq a) + +lemma bex_reg_left: + assumes a: "\x. R x \ Q x \ P x" + shows "Bex R Q \ Ex P" + by (metis COMBC_def Collect_def Collect_mem_eq a) + +lemma ball_reg_left: + assumes a: "equivp R" + shows "(\x. (Q x \ P x)) \ Ball (Respects R) Q \ All P" + by (metis equivp_reflp in_respects a) + +lemma bex_reg_right: + assumes a: "equivp R" + shows "(\x. (Q x \ P x)) \ Ex Q \ Bex (Respects R) P" + by (metis equivp_reflp in_respects a) + +lemma ball_reg_eqv_range: + fixes P::"'a \ bool" + and x::"'a" + assumes a: "equivp R2" + shows "(Ball (Respects (R1 ===> R2)) (\f. P (f x)) = All (\f. P (f x)))" + apply(rule iffI) + apply(rule allI) + apply(drule_tac x="\y. f x" in bspec) + apply(simp add: Respects_def in_respects) + apply(rule impI) + using a equivp_reflp_symp_transp[of "R2"] + apply(simp add: reflp_def) + apply(simp) + apply(simp) + done + +lemma bex_reg_eqv_range: + fixes P::"'a \ bool" + and x::"'a" + assumes a: "equivp R2" + shows "(Bex (Respects (R1 ===> R2)) (\f. P (f x)) = Ex (\f. P (f x)))" + apply(auto) + apply(rule_tac x="\y. f x" in bexI) + apply(simp) + apply(simp add: Respects_def in_respects) + apply(rule impI) + using a equivp_reflp_symp_transp[of "R2"] + apply(simp add: reflp_def) + done + +lemma all_reg: + assumes a: "!x :: 'a. (P x --> Q x)" + and b: "All P" + shows "All Q" + using a b by (metis) + +lemma ex_reg: + assumes a: "!x :: 'a. (P x --> Q x)" + and b: "Ex P" + shows "Ex Q" + using a b by (metis) + +lemma ball_reg: + assumes a: "!x :: 'a. (R x --> P x --> Q x)" + and b: "Ball R P" + shows "Ball R Q" + using a b by (metis COMBC_def Collect_def Collect_mem_eq) + +lemma bex_reg: + assumes a: "!x :: 'a. (R x --> P x --> Q x)" + and b: "Bex R P" + shows "Bex R Q" + using a b by (metis COMBC_def Collect_def Collect_mem_eq) + +lemma ball_all_comm: + "(\y. (\x\P. A x y) \ (\x. B x y)) \ ((\x\P. \y. A x y) \ (\x. \y. B x y))" +by auto + +lemma bex_ex_comm: + "((\y. \x. A x y) \ (\y. \x\P. B x y)) \ ((\x. \y. A x y) \ (\x\P. \y. B x y))" +by auto + +(* Bounded abstraction *) +definition + Babs :: "('a \ bool) \ ('a \ 'b) \ 'a \ 'b" +where + "(x \ p) \ (Babs p m x = m x)" + +(* 3 lemmas needed for proving repabs_inj *) +lemma ball_rsp: + assumes a: "(R ===> (op =)) f g" + shows "Ball (Respects R) f = Ball (Respects R) g" + using a by (simp add: Ball_def in_respects) + +lemma bex_rsp: + assumes a: "(R ===> (op =)) f g" + shows "(Bex (Respects R) f = Bex (Respects R) g)" + using a by (simp add: Bex_def in_respects) + +lemma babs_rsp: + assumes q: "Quotient R1 Abs1 Rep1" + and a: "(R1 ===> R2) f g" + shows "(R1 ===> R2) (Babs (Respects R1) f) (Babs (Respects R1) g)" + apply (auto simp add: Babs_def) + apply (subgoal_tac "x \ Respects R1 \ y \ Respects R1") + using a apply (simp add: Babs_def) + apply (simp add: in_respects) + using Quotient_rel[OF q] + by metis + +(* 2 lemmas needed for cleaning of quantifiers *) +lemma all_prs: + assumes a: "Quotient R absf repf" + shows "Ball (Respects R) ((absf ---> id) f) = All f" + using a unfolding Quotient_def + by (metis in_respects fun_map.simps id_apply) + +lemma ex_prs: + assumes a: "Quotient R absf repf" + shows "Bex (Respects R) ((absf ---> id) f) = Ex f" + using a unfolding Quotient_def + by (metis COMBC_def Collect_def Collect_mem_eq in_respects fun_map.simps id_apply) + +lemma fun_rel_id: + assumes a: "\x y. R1 x y \ R2 (f x) (g y)" + shows "(R1 ===> R2) f g" +using a by simp + +lemma quot_rel_rsp: + assumes a: "Quotient R Abs Rep" + shows "(R ===> R ===> op =) R R" + apply(rule fun_rel_id)+ + apply(rule equals_rsp[OF a]) + apply(assumption)+ + done + + + + + + +(******************************************) +(* REST OF THE FILE IS UNUSED (until now) *) +(******************************************) +lemma Quotient_rel_abs: + assumes a: "Quotient E Abs Rep" + shows "E r s \ Abs r = Abs s" +using a unfolding Quotient_def +by blast + +lemma Quotient_rel_abs_eq: + assumes a: "Quotient E Abs Rep" + shows "E r r \ E s s \ E r s = (Abs r = Abs s)" +using a unfolding Quotient_def +by blast + +lemma in_fun: + shows "x \ ((f ---> g) s) = g (f x \ s)" +by (simp add: mem_def) + +lemma RESPECTS_THM: + shows "Respects (R1 ===> R2) f = (\x y. R1 x y \ R2 (f x) (f y))" +unfolding Respects_def +by (simp add: expand_fun_eq) + +lemma RESPECTS_REP_ABS: + assumes a: "Quotient R1 Abs1 Rep1" + and b: "Respects (R1 ===> R2) f" + and c: "R1 x x" + shows "R2 (f (Rep1 (Abs1 x))) (f x)" +using a b[simplified RESPECTS_THM] c unfolding Quotient_def +by blast + +lemma RESPECTS_MP: + assumes a: "Respects (R1 ===> R2) f" + and b: "R1 x y" + shows "R2 (f x) (f y)" +using a b unfolding Respects_def +by simp + +lemma RESPECTS_o: + assumes a: "Respects (R2 ===> R3) f" + and b: "Respects (R1 ===> R2) g" + shows "Respects (R1 ===> R3) (f o g)" +using a b unfolding Respects_def +by simp + +lemma fun_rel_EQ_REL: + assumes q1: "Quotient R1 Abs1 Rep1" + and q2: "Quotient R2 Abs2 Rep2" + shows "(R1 ===> R2) f g = ((Respects (R1 ===> R2) f) \ (Respects (R1 ===> R2) g) + \ ((Rep1 ---> Abs2) f = (Rep1 ---> Abs2) g))" +using fun_quotient[OF q1 q2] unfolding Respects_def Quotient_def expand_fun_eq +by blast + +(* Not used since in the end we just unfold fun_map *) +lemma APP_PRS: + assumes q1: "Quotient R1 abs1 rep1" + and q2: "Quotient R2 abs2 rep2" + shows "abs2 ((abs1 ---> rep2) f (rep1 x)) = f x" +unfolding expand_fun_eq +using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2] +by simp + +(* Ask Peter: assumption q1 and q2 not used and lemma is the 'identity' *) +lemma LAMBDA_RSP: + assumes q1: "Quotient R1 Abs1 Rep1" + and q2: "Quotient R2 Abs2 Rep2" + and a: "(R1 ===> R2) f1 f2" + shows "(R1 ===> R2) (\x. f1 x) (\y. f2 y)" +by (rule a) + +(* ASK Peter about next four lemmas in quotientScript +lemma ABSTRACT_PRS: + assumes q1: "Quotient R1 Abs1 Rep1" + and q2: "Quotient R2 Abs2 Rep2" + shows "f = (Rep1 ---> Abs2) ???" +*) + + +lemma fun_rel_EQUALS: + assumes q1: "Quotient R1 Abs1 Rep1" + and q2: "Quotient R2 Abs2 Rep2" + and r1: "Respects (R1 ===> R2) f" + and r2: "Respects (R1 ===> R2) g" + shows "((Rep1 ---> Abs2) f = (Rep1 ---> Abs2) g) = (\x y. R1 x y \ R2 (f x) (g y))" +apply(rule_tac iffI) +using fun_quotient[OF q1 q2] r1 r2 unfolding Quotient_def Respects_def +apply(metis apply_rsp') +using r1 unfolding Respects_def expand_fun_eq +apply(simp (no_asm_use)) +apply(metis Quotient_rel[OF q2] Quotient_rel_rep[OF q1]) +done + +(* ask Peter: fun_rel_IMP used twice *) +lemma fun_rel_IMP2: + assumes q1: "Quotient R1 Abs1 Rep1" + and q2: "Quotient R2 Abs2 Rep2" + and r1: "Respects (R1 ===> R2) f" + and r2: "Respects (R1 ===> R2) g" + and a: "(Rep1 ---> Abs2) f = (Rep1 ---> Abs2) g" + shows "R1 x y \ R2 (f x) (g y)" +using q1 q2 r1 r2 a +by (simp add: fun_rel_EQUALS) + +lemma LAMBDA_REP_ABS_RSP: + assumes r1: "\r r'. R1 r r' \R1 r (Rep1 (Abs1 r'))" + and r2: "\r r'. R2 r r' \R2 r (Rep2 (Abs2 r'))" + shows "(R1 ===> R2) f1 f2 \ (R1 ===> R2) f1 ((Abs1 ---> Rep2) ((Rep1 ---> Abs2) f2))" +using r1 r2 by auto + +(* Not used *) +lemma rep_abs_rsp_left: + assumes q: "Quotient R Abs Rep" + and a: "R x1 x2" + shows "R x1 (Rep (Abs x2))" +using q a by (metis Quotient_rel[OF q] Quotient_abs_rep[OF q] Quotient_rep_reflp[OF q]) + + + +(* bool theory: COND, LET *) +lemma IF_PRS: + assumes q: "Quotient R Abs Rep" + shows "If a b c = Abs (If a (Rep b) (Rep c))" +using Quotient_abs_rep[OF q] by auto + +(* ask peter: no use of q *) +lemma IF_RSP: + assumes q: "Quotient R Abs Rep" + and a: "a1 = a2" "R b1 b2" "R c1 c2" + shows "R (If a1 b1 c1) (If a2 b2 c2)" +using a by auto + +lemma LET_PRS: + assumes q1: "Quotient R1 Abs1 Rep1" + and q2: "Quotient R2 Abs2 Rep2" + shows "Let x f = Abs2 (Let (Rep1 x) ((Abs1 ---> Rep2) f))" +using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2] by auto + +lemma LET_RSP: + assumes q1: "Quotient R1 Abs1 Rep1" + and a1: "(R1 ===> R2) f g" + and a2: "R1 x y" + shows "R2 ((Let x f)::'c) ((Let y g)::'c)" +using apply_rsp[OF q1 a1] a2 +by auto + + + +(* ask peter what are literal_case *) +(* literal_case_PRS *) +(* literal_case_RSP *) + + + + + +(* combinators: I, K, o, C, W *) + +(* We use id_simps which includes id_apply; so these 2 theorems can be removed *) + +lemma I_PRS: + assumes q: "Quotient R Abs Rep" + shows "id e = Abs (id (Rep e))" +using Quotient_abs_rep[OF q] by auto + +lemma I_RSP: + assumes q: "Quotient R Abs Rep" + and a: "R e1 e2" + shows "R (id e1) (id e2)" +using a by auto + +lemma o_PRS: + assumes q1: "Quotient R1 Abs1 Rep1" + and q2: "Quotient R2 Abs2 Rep2" + and q3: "Quotient R3 Abs3 Rep3" + shows "f o g = (Rep1 ---> Abs3) (((Abs2 ---> Rep3) f) o ((Abs1 ---> Rep2) g))" +using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2] Quotient_abs_rep[OF q3] +unfolding o_def expand_fun_eq +by simp + +lemma o_RSP: + assumes q1: "Quotient R1 Abs1 Rep1" + and q2: "Quotient R2 Abs2 Rep2" + and q3: "Quotient R3 Abs3 Rep3" + and a1: "(R2 ===> R3) f1 f2" + and a2: "(R1 ===> R2) g1 g2" + shows "(R1 ===> R3) (f1 o g1) (f2 o g2)" +using a1 a2 unfolding o_def expand_fun_eq +by (auto) + +lemma COND_PRS: + assumes a: "Quotient R absf repf" + shows "(if a then b else c) = absf (if a then repf b else repf c)" + using a unfolding Quotient_def by auto + + +end + diff -r 6088fea1c8b1 -r 8a1c8dc72b5c Quot/Quotients.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Quot/Quotients.thy Mon Dec 07 14:09:50 2009 +0100 @@ -0,0 +1,80 @@ +theory Quotients +imports Main +begin + +(* Other quotients that have not been proved yet *) + +fun + option_rel +where + "option_rel R None None = True" +| "option_rel R (Some x) None = False" +| "option_rel R None (Some x) = False" +| "option_rel R (Some x) (Some y) = R x y" + +fun + option_map +where + "option_map f None = None" +| "option_map f (Some x) = Some (f x)" + +fun + prod_rel +where + "prod_rel R1 R2 (a1,a2) (b1,b2) = (R1 a1 b1 \ R2 a2 b2)" + +fun + prod_map +where + "prod_map f1 f2 (a,b) = (f1 a, f2 b)" + +fun + sum_rel +where + "sum_rel R1 R2 (Inl a1) (Inl b1) = R1 a1 b1" +| "sum_rel R1 R2 (Inl a1) (Inr b2) = False" +| "sum_rel R1 R2 (Inr a2) (Inl b1) = False" +| "sum_rel R1 R2 (Inr a2) (Inr b2) = R2 a2 b2" + +fun + sum_map +where + "sum_map f1 f2 (Inl a) = Inl (f1 a)" +| "sum_map f1 f2 (Inr a) = Inr (f2 a)" + + + + + +fun + noption_map::"('a \ 'b) \ ('a noption) \ ('b noption)" +where + "noption_map f (nSome x) = nSome (f x)" +| "noption_map f nNone = nNone" + +fun + noption_rel +where + "noption_rel r (nSome x) (nSome y) = r x y" +| "noption_rel r _ _ = False" + +declare [[map noption = (noption_map, noption_rel)]] + +lemma "noption_map id = id" +sorry + +lemma noption_Quotient: + assumes q: "Quotient R Abs Rep" + shows "Quotient (noption_rel R) (noption_map Abs) (noption_map Rep)" + apply (unfold Quotient_def) + apply (auto) + using q + apply (unfold Quotient_def) + apply (case_tac "a :: 'b noption") + apply (simp) + apply (simp) + apply (case_tac "a :: 'b noption") + apply (simp only: option_map.simps) + apply (subst option_rel.simps) + (* Simp starts hanging so don't know how to continue *) + sorry diff -r 6088fea1c8b1 -r 8a1c8dc72b5c Quot/ROOT.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Quot/ROOT.ML Mon Dec 07 14:09:50 2009 +0100 @@ -0,0 +1,4 @@ +(* + no_document use_thys ["This_Theory1", "This_Theory2"]; + use_thys ["That_Theory1", "That_Theory2", "That_Theory3"]; +*) diff -r 6088fea1c8b1 -r 8a1c8dc72b5c QuotList.thy --- a/QuotList.thy Mon Dec 07 14:00:36 2009 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,174 +0,0 @@ -theory QuotList -imports QuotScript List -begin - -fun - list_rel -where - "list_rel R [] [] = True" -| "list_rel R (x#xs) [] = False" -| "list_rel R [] (x#xs) = False" -| "list_rel R (x#xs) (y#ys) = (R x y \ list_rel R xs ys)" - -lemma list_equivp: - assumes a: "equivp R" - shows "equivp (list_rel R)" - unfolding equivp_def - apply(rule allI)+ - apply(induct_tac x y rule: list_induct2') - apply(simp_all add: expand_fun_eq) - apply(metis list_rel.simps(1) list_rel.simps(2)) - apply(metis list_rel.simps(1) list_rel.simps(2)) - apply(rule iffI) - apply(rule allI) - apply(case_tac x) - apply(simp_all) - using a - apply(unfold equivp_def) - apply(auto)[1] - apply(metis list_rel.simps(4)) - done - -lemma list_rel_rel: - assumes q: "Quotient R Abs Rep" - shows "list_rel R r s = (list_rel R r r \ list_rel R s s \ (map Abs r = map Abs s))" - apply(induct r s rule: list_induct2') - apply(simp_all) - using Quotient_rel[OF q] - apply(metis) - done - -lemma list_quotient: - assumes q: "Quotient R Abs Rep" - shows "Quotient (list_rel R) (map Abs) (map Rep)" - unfolding Quotient_def - apply(rule conjI) - apply(rule allI) - apply(induct_tac a) - apply(simp) - apply(simp add: Quotient_abs_rep[OF q]) - apply(rule conjI) - apply(rule allI) - apply(induct_tac a) - apply(simp) - apply(simp) - apply(simp add: Quotient_rep_reflp[OF q]) - apply(rule allI)+ - apply(rule list_rel_rel[OF q]) - done - - -lemma cons_prs: - assumes q: "Quotient R Abs Rep" - shows "(map Abs) ((Rep h) # (map Rep t)) = h # t" -by (induct t) (simp_all add: Quotient_abs_rep[OF q]) - -lemma cons_rsp: - assumes q: "Quotient R Abs Rep" - shows "(R ===> list_rel R ===> list_rel R) op # op #" -by (auto) - -lemma nil_prs: - assumes q: "Quotient R Abs Rep" - shows "map Abs [] \ []" -by (simp) - -lemma nil_rsp: - assumes q: "Quotient R Abs Rep" - shows "list_rel R [] []" -by simp - -lemma map_prs: - assumes a: "Quotient R1 abs1 rep1" - and b: "Quotient R2 abs2 rep2" - shows "(map abs2) (map ((abs1 ---> rep2) f) (map rep1 l)) = map f l" -by (induct l) (simp_all add: Quotient_abs_rep[OF a] Quotient_abs_rep[OF b]) - -lemma map_rsp: - assumes q1: "Quotient R1 Abs1 Rep1" - and q2: "Quotient R2 Abs2 Rep2" - shows "((R1 ===> R2) ===> (list_rel R1) ===> list_rel R2) map map" -apply(simp) -apply(rule allI)+ -apply(rule impI) -apply(rule allI)+ -apply (induct_tac xa ya rule: list_induct2') -apply simp_all -done - -(* TODO: if the above is correct, we can remove this one *) -lemma map_rsp_lo: - assumes q1: "Quotient R1 Abs1 Rep1" - and q2: "Quotient R2 Abs2 Rep2" - and a: "(R1 ===> R2) f1 f2" - and b: "list_rel R1 l1 l2" - shows "list_rel R2 (map f1 l1) (map f2 l2)" -using b a -by (induct l1 l2 rule: list_induct2') (simp_all) - -lemma foldr_prs: - assumes a: "Quotient R1 abs1 rep1" - and b: "Quotient R2 abs2 rep2" - shows "abs2 (foldr ((abs1 ---> abs2 ---> rep2) f) (map rep1 l) (rep2 e)) = foldr f l e" -by (induct l) (simp_all add: Quotient_abs_rep[OF a] Quotient_abs_rep[OF b]) - -lemma foldl_prs: - assumes a: "Quotient R1 abs1 rep1" - and b: "Quotient R2 abs2 rep2" - shows "abs1 (foldl ((abs1 ---> abs2 ---> rep1) f) (rep1 e) (map rep2 l)) = foldl f e l" -by (induct l arbitrary:e) (simp_all add: Quotient_abs_rep[OF a] Quotient_abs_rep[OF b]) - -lemma list_rel_empty: "list_rel R [] b \ length b = 0" -by (induct b) (simp_all) - -lemma list_rel_len: "list_rel R a b \ length a = length b" -apply (induct a arbitrary: b) -apply (simp add: list_rel_empty) -apply (case_tac b) -apply simp_all -done - -(* TODO: induct_tac doesn't accept 'arbitrary'. - induct doesn't accept 'rule'. - that's why the proof uses manual generalisation and needs assumptions - both in conclusion for induction and in assumptions. *) -lemma foldl_rsp: - assumes q1: "Quotient R1 Abs1 Rep1" - and q2: "Quotient R2 Abs2 Rep2" - shows "((R1 ===> R2 ===> R1) ===> R1 ===> list_rel R2 ===> R1) foldl foldl" -apply auto -apply (subgoal_tac "R1 xa ya \ list_rel R2 xb yb \ R1 (foldl x xa xb) (foldl y ya yb)") -apply simp -apply (rule_tac x="xa" in spec) -apply (rule_tac x="ya" in spec) -apply (rule_tac xs="xb" and ys="yb" in list_induct2) -apply (rule list_rel_len) -apply (simp_all) -done - -(* TODO: foldr_rsp should be similar *) - - - - -(* TODO: Rest are unused *) - -lemma list_map_id: - shows "map (\x. x) = (\x. x)" - by simp - -lemma list_rel_eq: - shows "list_rel (op =) \ (op =)" -apply(rule eq_reflection) -unfolding expand_fun_eq -apply(rule allI)+ -apply(induct_tac x xa rule: list_induct2') -apply(simp_all) -done - -lemma list_rel_refl: - assumes a: "\x y. R x y = (R x = R y)" - shows "list_rel R x x" -by (induct x) (auto simp add: a) - -end diff -r 6088fea1c8b1 -r 8a1c8dc72b5c QuotMain.thy --- a/QuotMain.thy Mon Dec 07 14:00:36 2009 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,1191 +0,0 @@ -theory QuotMain -imports QuotScript QuotList QuotProd Prove -uses ("quotient_info.ML") - ("quotient.ML") - ("quotient_def.ML") -begin - - -locale QUOT_TYPE = - fixes R :: "'a \ 'a \ bool" - and Abs :: "('a \ bool) \ 'b" - and Rep :: "'b \ ('a \ bool)" - assumes equivp: "equivp R" - and rep_prop: "\y. \x. Rep y = R x" - and rep_inverse: "\x. Abs (Rep x) = x" - and abs_inverse: "\x. (Rep (Abs (R x))) = (R x)" - and rep_inject: "\x y. (Rep x = Rep y) = (x = y)" -begin - -definition - ABS::"'a \ 'b" -where - "ABS x \ Abs (R x)" - -definition - REP::"'b \ 'a" -where - "REP a = Eps (Rep a)" - -lemma lem9: - shows "R (Eps (R x)) = R x" -proof - - have a: "R x x" using equivp by (simp add: equivp_reflp_symp_transp reflp_def) - then have "R x (Eps (R x))" by (rule someI) - then show "R (Eps (R x)) = R x" - using equivp unfolding equivp_def by simp -qed - -theorem thm10: - shows "ABS (REP a) \ a" - apply (rule eq_reflection) - unfolding ABS_def REP_def -proof - - from rep_prop - obtain x where eq: "Rep a = R x" by auto - have "Abs (R (Eps (Rep a))) = Abs (R (Eps (R x)))" using eq by simp - also have "\ = Abs (R x)" using lem9 by simp - also have "\ = Abs (Rep a)" using eq by simp - also have "\ = a" using rep_inverse by simp - finally - show "Abs (R (Eps (Rep a))) = a" by simp -qed - -lemma REP_refl: - shows "R (REP a) (REP a)" -unfolding REP_def -by (simp add: equivp[simplified equivp_def]) - -lemma lem7: - shows "(R x = R y) = (Abs (R x) = Abs (R y))" -apply(rule iffI) -apply(simp) -apply(drule rep_inject[THEN iffD2]) -apply(simp add: abs_inverse) -done - -theorem thm11: - shows "R r r' = (ABS r = ABS r')" -unfolding ABS_def -by (simp only: equivp[simplified equivp_def] lem7) - - -lemma REP_ABS_rsp: - shows "R f (REP (ABS g)) = R f g" - and "R (REP (ABS g)) f = R g f" -by (simp_all add: thm10 thm11) - -lemma Quotient: - "Quotient R ABS REP" -apply(unfold Quotient_def) -apply(simp add: thm10) -apply(simp add: REP_refl) -apply(subst thm11[symmetric]) -apply(simp add: equivp[simplified equivp_def]) -done - -lemma R_trans: - assumes ab: "R a b" - and bc: "R b c" - shows "R a c" -proof - - have tr: "transp R" using equivp equivp_reflp_symp_transp[of R] by simp - moreover have ab: "R a b" by fact - moreover have bc: "R b c" by fact - ultimately show "R a c" unfolding transp_def by blast -qed - -lemma R_sym: - assumes ab: "R a b" - shows "R b a" -proof - - have re: "symp R" using equivp equivp_reflp_symp_transp[of R] by simp - then show "R b a" using ab unfolding symp_def by blast -qed - -lemma R_trans2: - assumes ac: "R a c" - and bd: "R b d" - shows "R a b = R c d" -using ac bd -by (blast intro: R_trans R_sym) - -lemma REPS_same: - shows "R (REP a) (REP b) \ (a = b)" -proof - - have "R (REP a) (REP b) = (a = b)" - proof - assume as: "R (REP a) (REP b)" - from rep_prop - obtain x y - where eqs: "Rep a = R x" "Rep b = R y" by blast - from eqs have "R (Eps (R x)) (Eps (R y))" using as unfolding REP_def by simp - then have "R x (Eps (R y))" using lem9 by simp - then have "R (Eps (R y)) x" using R_sym by blast - then have "R y x" using lem9 by simp - then have "R x y" using R_sym by blast - then have "ABS x = ABS y" using thm11 by simp - then have "Abs (Rep a) = Abs (Rep b)" using eqs unfolding ABS_def by simp - then show "a = b" using rep_inverse by simp - next - assume ab: "a = b" - have "reflp R" using equivp equivp_reflp_symp_transp[of R] by simp - then show "R (REP a) (REP b)" unfolding reflp_def using ab by auto - qed - then show "R (REP a) (REP b) \ (a = b)" by simp -qed - -end - -section {* type definition for the quotient type *} - -(* the auxiliary data for the quotient types *) -use "quotient_info.ML" - -declare [[map list = (map, list_rel)]] -declare [[map * = (prod_fun, prod_rel)]] -declare [[map "fun" = (fun_map, fun_rel)]] - -(* identity quotient is not here as it has to be applied first *) -lemmas [quotient_thm] = - fun_quotient list_quotient prod_quotient - -lemmas [quotient_rsp] = - quot_rel_rsp nil_rsp cons_rsp foldl_rsp pair_rsp - -(* fun_map is not here since equivp is not true *) -(* TODO: option, ... *) -lemmas [quotient_equiv] = - identity_equivp list_equivp prod_equivp - - -ML {* maps_lookup @{theory} "List.list" *} -ML {* maps_lookup @{theory} "*" *} -ML {* maps_lookup @{theory} "fun" *} - - -(* definition of the quotient types *) -(* FIXME: should be called quotient_typ.ML *) -use "quotient.ML" - - -(* lifting of constants *) -use "quotient_def.ML" - -section {* Simset setup *} - -(* since HOL_basic_ss is too "big", we need to set up *) -(* our own minimal simpset *) -ML {* -fun mk_minimal_ss ctxt = - Simplifier.context ctxt empty_ss - setsubgoaler asm_simp_tac - setmksimps (mksimps []) -*} - -section {* atomize *} - -lemma atomize_eqv[atomize]: - shows "(Trueprop A \ Trueprop B) \ (A \ B)" -proof - assume "A \ B" - then show "Trueprop A \ Trueprop B" by unfold -next - assume *: "Trueprop A \ Trueprop B" - have "A = B" - proof (cases A) - case True - have "A" by fact - then show "A = B" using * by simp - next - case False - have "\A" by fact - then show "A = B" using * by auto - qed - then show "A \ B" by (rule eq_reflection) -qed - -ML {* -fun atomize_thm thm = -let - val thm' = Thm.freezeT (forall_intr_vars thm) - val thm'' = ObjectLogic.atomize (cprop_of thm') -in - @{thm equal_elim_rule1} OF [thm'', thm'] -end -*} - -section {* infrastructure about id *} - -lemma prod_fun_id: "prod_fun id id \ id" - by (rule eq_reflection) (simp add: prod_fun_def) - -lemma map_id: "map id \ id" - apply (rule eq_reflection) - apply (rule ext) - apply (rule_tac list="x" in list.induct) - apply (simp_all) - done - -lemmas id_simps = - fun_map_id[THEN eq_reflection] - id_apply[THEN eq_reflection] - id_def[THEN eq_reflection,symmetric] - prod_fun_id map_id - -ML {* -fun simp_ids thm = - MetaSimplifier.rewrite_rule @{thms id_simps} thm -*} - -section {* Debugging infrastructure for testing tactics *} - -ML {* -fun my_print_tac ctxt s i thm = -let - val prem_str = nth (prems_of thm) (i - 1) - |> Syntax.string_of_term ctxt - handle Subscript => "no subgoal" - val _ = tracing (s ^ "\n" ^ prem_str) -in - Seq.single thm -end *} - -ML {* -fun DT ctxt s tac i thm = -let - val before_goal = nth (prems_of thm) (i - 1) - |> Syntax.string_of_term ctxt - val before_msg = ["before: " ^ s, before_goal, "after: " ^ s] - |> cat_lines -in - EVERY [tac i, my_print_tac ctxt before_msg i] thm -end - -fun NDT ctxt s tac thm = tac thm -*} - -section {* Matching of terms and types *} - -ML {* -fun matches_typ (ty, ty') = - case (ty, ty') of - (_, TVar _) => true - | (TFree x, TFree x') => x = x' - | (Type (s, tys), Type (s', tys')) => - s = s' andalso - if (length tys = length tys') - then (List.all matches_typ (tys ~~ tys')) - else false - | _ => false -*} - -ML {* -fun matches_term (trm, trm') = - case (trm, trm') of - (_, Var _) => true - | (Const (s, ty), Const (s', ty')) => s = s' andalso matches_typ (ty, ty') - | (Free (x, ty), Free (x', ty')) => x = x' andalso matches_typ (ty, ty') - | (Bound i, Bound j) => i = j - | (Abs (_, T, t), Abs (_, T', t')) => matches_typ (T, T') andalso matches_term (t, t') - | (t $ s, t' $ s') => matches_term (t, t') andalso matches_term (s, s') - | _ => false -*} - -section {* Infrastructure for collecting theorems for starting the lifting *} - -ML {* -fun lookup_quot_data lthy qty = - let - val qty_name = fst (dest_Type qty) - val SOME quotdata = quotdata_lookup lthy qty_name - (* TODO: Should no longer be needed *) - val rty = Logic.unvarifyT (#rtyp quotdata) - val rel = #rel quotdata - val rel_eqv = #equiv_thm quotdata - val rel_refl = @{thm equivp_reflp} OF [rel_eqv] - in - (rty, rel, rel_refl, rel_eqv) - end -*} - -ML {* -fun lookup_quot_thms lthy qty_name = - let - val thy = ProofContext.theory_of lthy; - val trans2 = PureThy.get_thm thy ("QUOT_TYPE_I_" ^ qty_name ^ ".R_trans2") - val reps_same = PureThy.get_thm thy ("QUOT_TYPE_I_" ^ qty_name ^ ".REPS_same") - val absrep = PureThy.get_thm thy ("QUOT_TYPE_I_" ^ qty_name ^ ".thm10") - val quot = PureThy.get_thm thy ("Quotient_" ^ qty_name) - in - (trans2, reps_same, absrep, quot) - end -*} - -section {* Regularization *} - -(* -Regularizing an rtrm means: - - quantifiers over a type that needs lifting are replaced by - bounded quantifiers, for example: - \x. P \ \x \ (Respects R). P / All (Respects R) P - - the relation R is given by the rty and qty; - - - abstractions over a type that needs lifting are replaced - by bounded abstractions: - \x. P \ Ball (Respects R) (\x. P) - - - equalities over the type being lifted are replaced by - corresponding relations: - A = B \ A \ B - - example with more complicated types of A, B: - A = B \ (op = \ op \) A B -*) - -ML {* -(* builds the relation that is the argument of respects *) -fun mk_resp_arg lthy (rty, qty) = -let - val thy = ProofContext.theory_of lthy -in - if rty = qty - then HOLogic.eq_const rty - else - case (rty, qty) of - (Type (s, tys), Type (s', tys')) => - if s = s' - then let - val SOME map_info = maps_lookup thy s - val args = map (mk_resp_arg lthy) (tys ~~ tys') - in - list_comb (Const (#relfun map_info, dummyT), args) - end - else let - val SOME qinfo = quotdata_lookup_thy thy s' - (* FIXME: check in this case that the rty and qty *) - (* FIXME: correspond to each other *) - val (s, _) = dest_Const (#rel qinfo) - (* FIXME: the relation should only be the string *) - (* FIXME: and the type needs to be calculated as below; *) - (* FIXME: maybe one should actually have a term *) - (* FIXME: and one needs to force it to have this type *) - in - Const (s, rty --> rty --> @{typ bool}) - end - | _ => HOLogic.eq_const dummyT - (* FIXME: check that the types correspond to each other? *) -end -*} - -ML {* -val mk_babs = Const (@{const_name Babs}, dummyT) -val mk_ball = Const (@{const_name Ball}, dummyT) -val mk_bex = Const (@{const_name Bex}, dummyT) -val mk_resp = Const (@{const_name Respects}, dummyT) -*} - -ML {* -(* - applies f to the subterm of an abstraction, *) -(* otherwise to the given term, *) -(* - used by regularize, therefore abstracted *) -(* variables do not have to be treated specially *) - -fun apply_subt f trm1 trm2 = - case (trm1, trm2) of - (Abs (x, T, t), Abs (x', T', t')) => Abs (x, T, f t t') - | _ => f trm1 trm2 - -(* the major type of All and Ex quantifiers *) -fun qnt_typ ty = domain_type (domain_type ty) -*} - -ML {* -(* produces a regularized version of rtm *) -(* - the result is still not completely typed *) -(* - does not need any special treatment of *) -(* bound variables *) - -fun regularize_trm lthy rtrm qtrm = - case (rtrm, qtrm) of - (Abs (x, ty, t), Abs (x', ty', t')) => - let - val subtrm = Abs(x, ty, regularize_trm lthy t t') - in - if ty = ty' - then subtrm - else mk_babs $ (mk_resp $ mk_resp_arg lthy (ty, ty')) $ subtrm - end - - | (Const (@{const_name "All"}, ty) $ t, Const (@{const_name "All"}, ty') $ t') => - let - val subtrm = apply_subt (regularize_trm lthy) t t' - in - if ty = ty' - then Const (@{const_name "All"}, ty) $ subtrm - else mk_ball $ (mk_resp $ mk_resp_arg lthy (qnt_typ ty, qnt_typ ty')) $ subtrm - end - - | (Const (@{const_name "Ex"}, ty) $ t, Const (@{const_name "Ex"}, ty') $ t') => - let - val subtrm = apply_subt (regularize_trm lthy) t t' - in - if ty = ty' - then Const (@{const_name "Ex"}, ty) $ subtrm - else mk_bex $ (mk_resp $ mk_resp_arg lthy (qnt_typ ty, qnt_typ ty')) $ subtrm - end - - | (* equalities need to be replaced by appropriate equivalence relations *) - (Const (@{const_name "op ="}, ty), Const (@{const_name "op ="}, ty')) => - if ty = ty' - then rtrm - else mk_resp_arg lthy (domain_type ty, domain_type ty') - - | (* in this case we check whether the given equivalence relation is correct *) - (rel, Const (@{const_name "op ="}, ty')) => - let - val exc = LIFT_MATCH "regularise (relation mismatch)" - val rel_ty = (fastype_of rel) handle TERM _ => raise exc - val rel' = mk_resp_arg lthy (domain_type rel_ty, domain_type ty') - in - if rel' = rel - then rtrm - else raise exc - end - | (_, Const (s, _)) => - let - fun same_name (Const (s, _)) (Const (s', _)) = (s = s') - | same_name _ _ = false - in - if same_name rtrm qtrm - then rtrm - else - let - fun exc1 s = LIFT_MATCH ("regularize (constant " ^ s ^ " not found)") - val exc2 = LIFT_MATCH ("regularize (constant mismatch)") - val thy = ProofContext.theory_of lthy - val rtrm' = (#rconst (qconsts_lookup thy s)) handle NotFound => raise (exc1 s) - in - if matches_term (rtrm, rtrm') - then rtrm - else raise exc2 - end - end - - | (t1 $ t2, t1' $ t2') => - (regularize_trm lthy t1 t1') $ (regularize_trm lthy t2 t2') - - | (Free (x, ty), Free (x', ty')) => - (* this case cannot arrise as we start with two fully atomized terms *) - raise (LIFT_MATCH "regularize (frees)") - - | (Bound i, Bound i') => - if i = i' - then rtrm - else raise (LIFT_MATCH "regularize (bounds mismatch)") - - | (rt, qt) => - raise (LIFT_MATCH "regularize (default)") -*} - -ML {* -fun equiv_tac ctxt = - REPEAT_ALL_NEW (FIRST' - [resolve_tac (equiv_rules_get ctxt)]) -*} - -ML {* -fun equiv_solver_tac ss = equiv_tac (Simplifier.the_context ss) -val equiv_solver = Simplifier.mk_solver' "Equivalence goal solver" equiv_solver_tac -*} - -ML {* -fun prep_trm thy (x, (T, t)) = - (cterm_of thy (Var (x, T)), cterm_of thy t) - -fun prep_ty thy (x, (S, ty)) = - (ctyp_of thy (TVar (x, S)), ctyp_of thy ty) -*} - -ML {* -fun matching_prs thy pat trm = -let - val univ = Unify.matchers thy [(pat, trm)] - val SOME (env, _) = Seq.pull univ - val tenv = Vartab.dest (Envir.term_env env) - val tyenv = Vartab.dest (Envir.type_env env) -in - (map (prep_ty thy) tyenv, map (prep_trm thy) tenv) -end -*} - -ML {* -fun calculate_instance ctxt thm redex R1 R2 = -let - val thy = ProofContext.theory_of ctxt - val goal = Const (@{const_name "equivp"}, dummyT) $ R2 - |> Syntax.check_term ctxt - |> HOLogic.mk_Trueprop - val eqv_prem = Goal.prove ctxt [] [] goal (fn {context,...} => equiv_tac context 1) - val thm = (@{thm eq_reflection} OF [thm OF [eqv_prem]]) - val R1c = cterm_of thy R1 - val thmi = Drule.instantiate' [] [SOME R1c] thm - val inst = matching_prs thy (term_of (Thm.lhs_of thmi)) redex - val thm2 = Drule.eta_contraction_rule (Drule.instantiate inst thmi) -in - SOME thm2 -end -handle _ => NONE -(* FIXME/TODO: what is the place where the exception can be raised: matching_prs? *) -*} - -ML {* -fun ball_bex_range_simproc ss redex = -let - val ctxt = Simplifier.the_context ss -in - case redex of - (Const (@{const_name "Ball"}, _) $ (Const (@{const_name "Respects"}, _) $ - (Const (@{const_name "fun_rel"}, _) $ R1 $ R2)) $ _) => - calculate_instance ctxt @{thm ball_reg_eqv_range} redex R1 R2 - | (Const (@{const_name "Bex"}, _) $ (Const (@{const_name "Respects"}, _) $ - (Const (@{const_name "fun_rel"}, _) $ R1 $ R2)) $ _) => - calculate_instance ctxt @{thm bex_reg_eqv_range} redex R1 R2 - | _ => NONE -end -*} - -lemma eq_imp_rel: - shows "equivp R \ a = b \ R a b" -by (simp add: equivp_reflp) - -(* FIXME/TODO: How does regularizing work? *) -(* FIXME/TODO: needs to be adapted - -To prove that the raw theorem implies the regularised one, -we try in order: - - - Reflexivity of the relation - - Assumption - - Elimnating quantifiers on both sides of toplevel implication - - Simplifying implications on both sides of toplevel implication - - Ball (Respects ?E) ?P = All ?P - - (\x. ?R x \ ?P x \ ?Q x) \ All ?P \ Ball ?R ?Q - -*) -ML {* -fun regularize_tac ctxt = -let - val thy = ProofContext.theory_of ctxt - val pat_ball = @{term "Ball (Respects (R1 ===> R2)) P"} - val pat_bex = @{term "Bex (Respects (R1 ===> R2)) P"} - val simproc = Simplifier.simproc_i thy "" [pat_ball, pat_bex] (K (ball_bex_range_simproc)) - val simpset = (mk_minimal_ss ctxt) - addsimps @{thms ball_reg_eqv bex_reg_eqv} - addsimprocs [simproc] addSolver equiv_solver - (* TODO: Make sure that there are no list_rel, pair_rel etc involved *) - val eq_eqvs = map (fn x => @{thm eq_imp_rel} OF [x]) (equiv_rules_get ctxt) -in - ObjectLogic.full_atomize_tac THEN' - simp_tac simpset THEN' - REPEAT_ALL_NEW (FIRST' [ - rtac @{thm ball_reg_right}, - rtac @{thm bex_reg_left}, - resolve_tac (Inductive.get_monos ctxt), - rtac @{thm ball_all_comm}, - rtac @{thm bex_ex_comm}, - resolve_tac eq_eqvs, - simp_tac simpset]) -end -*} - -section {* Injections of rep and abses *} - -(* -Injecting repabs means: - - For abstractions: - * If the type of the abstraction doesn't need lifting we recurse. - * If it does we add RepAbs around the whole term and check if the - variable needs lifting. - * If it doesn't then we recurse - * If it does we recurse and put 'RepAbs' around all occurences - of the variable in the obtained subterm. This in combination - with the RepAbs above will let us change the type of the - abstraction with rewriting. - For applications: - * If the term is 'Respects' applied to anything we leave it unchanged - * If the term needs lifting and the head is a constant that we know - how to lift, we put a RepAbs and recurse - * If the term needs lifting and the head is a free applied to subterms - (if it is not applied we treated it in Abs branch) then we - put RepAbs and recurse - * Otherwise just recurse. -*) - -ML {* -fun mk_repabs lthy (T, T') trm = - Quotient_Def.get_fun repF lthy (T, T') - $ (Quotient_Def.get_fun absF lthy (T, T') $ trm) -*} - -ML {* -(* bound variables need to be treated properly, *) -(* as the type of subterms need to be calculated *) -(* in the abstraction case *) - -fun inj_repabs_trm lthy (rtrm, qtrm) = - case (rtrm, qtrm) of - (Const (@{const_name "Ball"}, T) $ r $ t, Const (@{const_name "All"}, _) $ t') => - Const (@{const_name "Ball"}, T) $ r $ (inj_repabs_trm lthy (t, t')) - - | (Const (@{const_name "Bex"}, T) $ r $ t, Const (@{const_name "Ex"}, _) $ t') => - Const (@{const_name "Bex"}, T) $ r $ (inj_repabs_trm lthy (t, t')) - - | (Const (@{const_name "Babs"}, T) $ r $ t, t' as (Abs _)) => - Const (@{const_name "Babs"}, T) $ r $ (inj_repabs_trm lthy (t, t')) - - | (Abs (x, T, t), Abs (x', T', t')) => - let - val rty = fastype_of rtrm - val qty = fastype_of qtrm - val (y, s) = Term.dest_abs (x, T, t) - val (_, s') = Term.dest_abs (x', T', t') - val yvar = Free (y, T) - val result = Term.lambda_name (y, yvar) (inj_repabs_trm lthy (s, s')) - in - if rty = qty - then result - else mk_repabs lthy (rty, qty) result - end - - | (t $ s, t' $ s') => - (inj_repabs_trm lthy (t, t')) $ (inj_repabs_trm lthy (s, s')) - - | (Free (_, T), Free (_, T')) => - if T = T' - then rtrm - else mk_repabs lthy (T, T') rtrm - - | (_, Const (@{const_name "op ="}, _)) => rtrm - - (* FIXME: check here that rtrm is the corresponding definition for the const *) - | (_, Const (_, T')) => - let - val rty = fastype_of rtrm - in - if rty = T' - then rtrm - else mk_repabs lthy (rty, T') rtrm - end - - | _ => raise (LIFT_MATCH "injection") -*} - -section {* RepAbs Injection Tactic *} - -ML {* -fun quotient_tac ctxt = - REPEAT_ALL_NEW (FIRST' - [rtac @{thm identity_quotient}, - resolve_tac (quotient_rules_get ctxt)]) -*} - -(* solver for the simplifier *) -ML {* -fun quotient_solver_tac ss = quotient_tac (Simplifier.the_context ss) -val quotient_solver = Simplifier.mk_solver' "Quotient goal solver" quotient_solver_tac -*} - -ML {* -fun solve_quotient_assums ctxt thm = - let val gl = hd (Drule.strip_imp_prems (cprop_of thm)) in - thm OF [Goal.prove_internal [] gl (fn _ => quotient_tac ctxt 1)] - end - handle _ => error "solve_quotient_assums failed. Maybe a quotient_thm is missing" -*} - -(* Not used *) -(* It proves the Quotient assumptions by calling quotient_tac *) -ML {* -fun solve_quotient_assum i ctxt thm = - let - val tac = - (compose_tac (false, thm, i)) THEN_ALL_NEW - (quotient_tac ctxt); - val gc = Drule.strip_imp_concl (cprop_of thm); - in - Goal.prove_internal [] gc (fn _ => tac 1) - end - handle _ => error "solve_quotient_assum" -*} - -definition - "QUOT_TRUE x \ True" - -ML {* -fun find_qt_asm asms = - let - fun find_fun trm = - case trm of - (Const(@{const_name Trueprop}, _) $ (Const (@{const_name QUOT_TRUE}, _) $ _)) => true - | _ => false - in - case find_first find_fun asms of - SOME (_ $ (_ $ (f $ a))) => (f, a) - | SOME _ => error "find_qt_asm: no pair" - | NONE => error "find_qt_asm: no assumption" - end -*} - -(* -To prove that the regularised theorem implies the abs/rep injected, -we try: - - 1) theorems 'trans2' from the appropriate QUOT_TYPE - 2) remove lambdas from both sides: lambda_rsp_tac - 3) remove Ball/Bex from the right hand side - 4) use user-supplied RSP theorems - 5) remove rep_abs from the right side - 6) reflexivity of equality - 7) split applications of lifted type (apply_rsp) - 8) split applications of non-lifted type (cong_tac) - 9) apply extentionality - A) reflexivity of the relation - B) assumption - (Lambdas under respects may have left us some assumptions) - C) proving obvious higher order equalities by simplifying fun_rel - (not sure if it is still needed?) - D) unfolding lambda on one side - E) simplifying (= ===> =) for simpler respectfulness - -*) - -lemma quot_true_dests: - shows QT_all: "QUOT_TRUE (All P) \ QUOT_TRUE P" - and QT_ex: "QUOT_TRUE (Ex P) \ QUOT_TRUE P" - and QT_lam: "QUOT_TRUE (\x. P x) \ (\x. QUOT_TRUE (P x))" - and QT_ext: "(\x. QUOT_TRUE (a x) \ f x = g x) \ (QUOT_TRUE a \ f = g)" -apply(simp_all add: QUOT_TRUE_def ext) -done - -lemma QUOT_TRUE_i: "(QUOT_TRUE (a :: bool) \ P) \ P" -by (simp add: QUOT_TRUE_def) - -lemma QUOT_TRUE_imp: "QUOT_TRUE a \ QUOT_TRUE b" -by (simp add: QUOT_TRUE_def) - -ML {* -fun quot_true_conv1 ctxt fnctn ctrm = - case (term_of ctrm) of - (Const (@{const_name QUOT_TRUE}, _) $ x) => - let - val fx = fnctn x; - val thy = ProofContext.theory_of ctxt; - val cx = cterm_of thy x; - val cfx = cterm_of thy fx; - val cxt = ctyp_of thy (fastype_of x); - val cfxt = ctyp_of thy (fastype_of fx); - val thm = Drule.instantiate' [SOME cxt, SOME cfxt] [SOME cx, SOME cfx] @{thm QUOT_TRUE_imp} - in - Conv.rewr_conv thm ctrm - end -*} - -ML {* -fun quot_true_conv ctxt fnctn ctrm = - case (term_of ctrm) of - (Const (@{const_name QUOT_TRUE}, _) $ _) => - quot_true_conv1 ctxt fnctn ctrm - | _ $ _ => Conv.comb_conv (quot_true_conv ctxt fnctn) ctrm - | Abs _ => Conv.abs_conv (fn (_, ctxt) => quot_true_conv ctxt fnctn) ctxt ctrm - | _ => Conv.all_conv ctrm -*} - -ML {* -fun quot_true_tac ctxt fnctn = CONVERSION - ((Conv.params_conv ~1 (fn ctxt => - (Conv.prems_conv ~1 (quot_true_conv ctxt fnctn)))) ctxt) -*} - -ML {* fun dest_comb (f $ a) = (f, a) *} -ML {* fun dest_bcomb ((_ $ l) $ r) = (l, r) *} -(* TODO: Can this be done easier? *) -ML {* -fun unlam t = - case t of - (Abs a) => snd (Term.dest_abs a) - | _ => unlam (Abs("", domain_type (fastype_of t), (incr_boundvars 1 t) $ (Bound 0))) -*} - -ML {* -fun dest_fun_type (Type("fun", [T, S])) = (T, S) - | dest_fun_type _ = error "dest_fun_type" -*} - -ML {* -val bare_concl = HOLogic.dest_Trueprop o Logic.strip_assums_concl -*} - -ML {* -val apply_rsp_tac = - Subgoal.FOCUS (fn {concl, asms, context,...} => - case ((HOLogic.dest_Trueprop (term_of concl))) of - ((R2 $ (f $ x) $ (g $ y))) => - (let - val (asmf, asma) = find_qt_asm (map term_of asms); - in - if (fastype_of asmf) = (fastype_of f) then no_tac else let - val ty_a = fastype_of x; - val ty_b = fastype_of asma; - val ty_c = range_type (type_of f); - val thy = ProofContext.theory_of context; - val ty_inst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c]; - val thm = Drule.instantiate' ty_inst [] @{thm apply_rsp} - val te = solve_quotient_assums context thm - val t_inst = map (SOME o (cterm_of thy)) [R2, f, g, x, y]; - val thm = Drule.instantiate' [] t_inst te - in - compose_tac (false, thm, 2) 1 - end - end - handle ERROR "find_qt_asm: no pair" => no_tac) - | _ => no_tac) -*} -ML {* -fun SOLVES' tac = tac THEN_ALL_NEW (fn _ => no_tac) -*} - -ML {* -fun rep_abs_rsp_tac ctxt = - SUBGOAL (fn (goal, i) => - case (bare_concl goal) of - (rel $ _ $ (rep $ (abs $ _))) => - (let - val thy = ProofContext.theory_of ctxt; - val (ty_a, ty_b) = dest_fun_type (fastype_of abs); - val ty_inst = map (SOME o (ctyp_of thy)) [ty_a, ty_b]; - val t_inst = map (SOME o (cterm_of thy)) [rel, abs, rep]; - val thm = Drule.instantiate' ty_inst t_inst @{thm rep_abs_rsp} - val te = solve_quotient_assums ctxt thm - in - rtac te i - end - handle _ => no_tac) - | _ => no_tac) -*} - -ML {* -fun inj_repabs_tac_match ctxt trans2 = SUBGOAL (fn (goal, i) => -(case (bare_concl goal) of - (* (R1 ===> R2) (\x\) (\y\) ----> \R1 x y\ \ R2 (\x) (\y) *) - ((Const (@{const_name fun_rel}, _) $ _ $ _) $ (Abs _) $ (Abs _)) - => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam - - (* (op =) (Ball\) (Ball\) ----> (op =) (\) (\) *) -| (Const (@{const_name "op ="},_) $ - (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ - (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _)) - => rtac @{thm ball_rsp} THEN' dtac @{thm QT_all} - - (* (R1 ===> op =) (Ball\) (Ball\) ----> \R1 x y\ \ (Ball\x) = (Ball\y) *) -| (Const (@{const_name fun_rel}, _) $ _ $ _) $ - (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ - (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) - => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam - - (* (op =) (Bex\) (Bex\) ----> (op =) (\) (\) *) -| Const (@{const_name "op ="},_) $ - (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ - (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) - => rtac @{thm bex_rsp} THEN' dtac @{thm QT_ex} - - (* (R1 ===> op =) (Bex\) (Bex\) ----> \R1 x y\ \ (Bex\x) = (Bex\y) *) -| (Const (@{const_name fun_rel}, _) $ _ $ _) $ - (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ - (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) - => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam - -| (_ $ - (Const(@{const_name Babs},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $ - (Const(@{const_name Babs},_) $ (Const (@{const_name Respects}, _) $ _) $ _)) - => rtac @{thm babs_rsp} THEN' RANGE [quotient_tac ctxt] - - (* reflexivity of operators arising from Cong_tac *) -| Const (@{const_name "op ="},_) $ _ $ _ - => rtac @{thm refl} ORELSE' - (resolve_tac trans2 THEN' RANGE [ - quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)]) - -(* TODO: These patterns should should be somehow combined and generalized... *) -| (Const (@{const_name fun_rel}, _) $ _ $ _) $ - (Const (@{const_name fun_rel}, _) $ _ $ _) $ - (Const (@{const_name fun_rel}, _) $ _ $ _) - => rtac @{thm quot_rel_rsp} THEN_ALL_NEW quotient_tac ctxt - -| (Const (@{const_name fun_rel}, _) $ _ $ _) $ - (Const (@{const_name prod_rel}, _) $ _ $ _) $ - (Const (@{const_name prod_rel}, _) $ _ $ _) - => rtac @{thm quot_rel_rsp} THEN_ALL_NEW quotient_tac ctxt - - (* respectfulness of constants; in particular of a simple relation *) -| _ $ (Const _) $ (Const _) (* fun_rel, list_rel, etc but not equality *) - => resolve_tac (rsp_rules_get ctxt) THEN_ALL_NEW quotient_tac ctxt - - (* R (\) (Rep (Abs \)) ----> R (\) (\) *) - (* observe ---> *) -| _ $ _ $ _ - => rep_abs_rsp_tac ctxt - -| _ => error "inj_repabs_tac not a relation" -) i) -*} - -ML {* -fun inj_repabs_tac ctxt rel_refl trans2 = - (FIRST' [ - inj_repabs_tac_match ctxt trans2, - (* R (t $ \) (t' $ \) ----> apply_rsp provided type of t needs lifting *) - NDT ctxt "A" (apply_rsp_tac ctxt THEN' - (RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)])), - (* (op =) (t $ \) (t' $ \) ----> Cong provided type of t does not need lifting *) - (* merge with previous tactic *) - NDT ctxt "B" (Cong_Tac.cong_tac @{thm cong} THEN' - (RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)])), - (* (op =) (\x\) (\x\) ----> (op =) (\) (\) *) - NDT ctxt "C" (rtac @{thm ext} THEN' quot_true_tac ctxt unlam), - (* resolving with R x y assumptions *) - NDT ctxt "E" (atac), - (* reflexivity of the basic relations *) - (* R \ \ *) - NDT ctxt "D" (resolve_tac rel_refl) - ]) -*} - -ML {* -fun all_inj_repabs_tac ctxt rel_refl trans2 = - REPEAT_ALL_NEW (inj_repabs_tac ctxt rel_refl trans2) -*} - -section {* Cleaning of the theorem *} - -ML {* -fun make_inst lhs t = - let - val _ $ (Abs (_, _, (f as Var (_, Type ("fun", [T, _]))) $ u)) = lhs; - val _ $ (Abs (_, _, g)) = t; - fun mk_abs i t = - if incr_boundvars i u aconv t then Bound i - else (case t of - t1 $ t2 => mk_abs i t1 $ mk_abs i t2 - | Abs (s, T, t') => Abs (s, T, mk_abs (i + 1) t') - | Bound j => if i = j then error "make_inst" else t - | _ => t); - in (f, Abs ("x", T, mk_abs 0 g)) end; -*} - -ML {* -fun lambda_prs_simple_conv ctxt ctrm = - case (term_of ctrm) of - ((Const (@{const_name fun_map}, _) $ r1 $ (a2 as (Const (s,_)))) $ (Abs _)) => - let - val thy = ProofContext.theory_of ctxt - val (ty_b, ty_a) = dest_fun_type (fastype_of r1) - val (ty_c, ty_d) = dest_fun_type (fastype_of a2) - val tyinst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c, ty_d] - val tinst = [NONE, NONE, SOME (cterm_of thy r1), NONE, SOME (cterm_of thy a2)] - val lpi = Drule.instantiate' tyinst tinst @{thm lambda_prs} - val te = @{thm eq_reflection} OF [solve_quotient_assums ctxt (solve_quotient_assums ctxt lpi)] - val ts = MetaSimplifier.rewrite_rule @{thms id_simps} te - val _ = tracing ("te rule:\n" ^ (Syntax.string_of_term ctxt (prop_of te))); - val tl = Thm.lhs_of ts - val (insp, inst) = make_inst (term_of tl) (term_of ctrm) - val ti = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts - val _ = if not (s = @{const_name "id"}) then - (tracing "lambda_prs"; - tracing ("redex:\n" ^ (Syntax.string_of_term ctxt (term_of ctrm))); - tracing ("lpi rule:\n" ^ (Syntax.string_of_term ctxt (prop_of lpi))); - tracing ("te rule:\n" ^ (Syntax.string_of_term ctxt (prop_of te))); - tracing ("ts rule:\n" ^ (Syntax.string_of_term ctxt (prop_of ts))); - tracing ("instantiated rule:\n" ^ (Syntax.string_of_term ctxt (prop_of ti)))) - else () - in - Conv.rewr_conv ti ctrm - end - | _ => Conv.all_conv ctrm -*} - -ML {* -val lambda_prs_conv = - More_Conv.top_conv lambda_prs_simple_conv - -fun lambda_prs_tac ctxt = CONVERSION (lambda_prs_conv ctxt) -*} - -(* - Cleaning the theorem consists of three rewriting steps. - The first two need to be done before fun_map is unfolded - - 1) lambda_prs: - (Rep1 ---> Abs2) (\x. Rep2 (f (Abs1 x))) ----> f - - Implemented as conversion since it is not a pattern. - - 2) all_prs (the same for exists): - Ball (Respects R) ((abs ---> id) f) ----> All f - - Rewriting with definitions from the argument defs - (rep ---> abs) oldConst ----> newconst - - 3) Quotient_rel_rep: - Rel (Rep x) (Rep y) ----> x = y - - Quotient_abs_rep: - Abs (Rep x) ----> x - - id_simps; fun_map.simps -*) - -ML {* -fun clean_tac lthy = - let - val thy = ProofContext.theory_of lthy; - val defs = map (Thm.varifyT o symmetric o #def) (qconsts_dest thy) - (* FIXME: shouldn't the definitions already be varified? *) - val thms1 = @{thms all_prs ex_prs} @ defs - val thms2 = @{thms eq_reflection[OF fun_map.simps]} - @ @{thms id_simps Quotient_abs_rep Quotient_rel_rep} - fun simps thms = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver - in - EVERY' [lambda_prs_tac lthy, - simp_tac (simps thms1), - simp_tac (simps thms2), - TRY o rtac refl] - end -*} - -section {* Genralisation of free variables in a goal *} - -ML {* -fun inst_spec ctrm = - Drule.instantiate' [SOME (ctyp_of_term ctrm)] [NONE, SOME ctrm] @{thm spec} - -fun inst_spec_tac ctrms = - EVERY' (map (dtac o inst_spec) ctrms) - -fun all_list xs trm = - fold (fn (x, T) => fn t' => HOLogic.mk_all (x, T, t')) xs trm - -fun apply_under_Trueprop f = - HOLogic.dest_Trueprop #> f #> HOLogic.mk_Trueprop - -fun gen_frees_tac ctxt = - SUBGOAL (fn (concl, i) => - let - val thy = ProofContext.theory_of ctxt - val vrs = Term.add_frees concl [] - val cvrs = map (cterm_of thy o Free) vrs - val concl' = apply_under_Trueprop (all_list vrs) concl - val goal = Logic.mk_implies (concl', concl) - val rule = Goal.prove ctxt [] [] goal - (K (EVERY1 [inst_spec_tac (rev cvrs), atac])) - in - rtac rule i - end) -*} - -section {* General outline of the lifting procedure *} - -(* - A is the original raw theorem *) -(* - B is the regularized theorem *) -(* - C is the rep/abs injected version of B *) -(* - D is the lifted theorem *) -(* *) -(* - b is the regularization step *) -(* - c is the rep/abs injection step *) -(* - d is the cleaning part *) - -lemma lifting_procedure: - assumes a: "A" - and b: "A \ B" - and c: "B = C" - and d: "C = D" - shows "D" - using a b c d - by simp - -ML {* -fun lift_match_error ctxt fun_str rtrm qtrm = -let - val rtrm_str = Syntax.string_of_term ctxt rtrm - val qtrm_str = Syntax.string_of_term ctxt qtrm - val msg = [enclose "[" "]" fun_str, "The quotient theorem\n", qtrm_str, - "and the lifted theorem\n", rtrm_str, "do not match"] -in - error (space_implode " " msg) -end -*} - -ML {* -fun procedure_inst ctxt rtrm qtrm = -let - val thy = ProofContext.theory_of ctxt - val rtrm' = HOLogic.dest_Trueprop rtrm - val qtrm' = HOLogic.dest_Trueprop qtrm - val reg_goal = - Syntax.check_term ctxt (regularize_trm ctxt rtrm' qtrm') - handle (LIFT_MATCH s) => lift_match_error ctxt s rtrm qtrm - val _ = warning "Regularization done." - val inj_goal = - Syntax.check_term ctxt (inj_repabs_trm ctxt (reg_goal, qtrm')) - handle (LIFT_MATCH s) => lift_match_error ctxt s rtrm qtrm - val _ = warning "RepAbs Injection done." -in - Drule.instantiate' [] - [SOME (cterm_of thy rtrm'), - SOME (cterm_of thy reg_goal), - SOME (cterm_of thy inj_goal)] @{thm lifting_procedure} -end -*} - -(* Left for debugging *) -ML {* -fun procedure_tac ctxt rthm = - ObjectLogic.full_atomize_tac - THEN' gen_frees_tac ctxt - THEN' CSUBGOAL (fn (gl, i) => - let - val rthm' = atomize_thm rthm - val rule = procedure_inst ctxt (prop_of rthm') (term_of gl) - val thm = Drule.instantiate' [] [SOME (snd (Thm.dest_comb gl))] @{thm QUOT_TRUE_i} - in - (rtac rule THEN' RANGE [rtac rthm', (fn _ => all_tac), rtac thm]) i - end) -*} - -ML {* -(* FIXME/TODO should only get as arguments the rthm like procedure_tac *) - -fun lift_tac ctxt rthm = - ObjectLogic.full_atomize_tac - THEN' gen_frees_tac ctxt - THEN' CSUBGOAL (fn (gl, i) => - let - val rthm' = atomize_thm rthm - val rule = procedure_inst ctxt (prop_of rthm') (term_of gl) - val rel_refl = map (fn x => @{thm equivp_reflp} OF [x]) (equiv_rules_get ctxt) - val quotients = quotient_rules_get ctxt - val trans2 = map (fn x => @{thm equals_rsp} OF [x]) quotients - val thm = Drule.instantiate' [] [SOME (snd (Thm.dest_comb gl))] @{thm QUOT_TRUE_i} - in - (rtac rule THEN' - RANGE [rtac rthm', - regularize_tac ctxt, - rtac thm THEN' all_inj_repabs_tac ctxt rel_refl trans2, - clean_tac ctxt]) i - end) -*} - -end - diff -r 6088fea1c8b1 -r 8a1c8dc72b5c QuotProd.thy --- a/QuotProd.thy Mon Dec 07 14:00:36 2009 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,80 +0,0 @@ -theory QuotProd -imports QuotScript -begin - -fun - prod_rel -where - "prod_rel r1 r2 = (\(a,b) (c,d). r1 a c \ r2 b d)" - -(* prod_fun is a good mapping function *) - -lemma prod_equivp: - assumes a: "equivp R1" - assumes b: "equivp R2" - shows "equivp (prod_rel R1 R2)" -unfolding equivp_reflp_symp_transp reflp_def symp_def transp_def -apply(auto simp add: equivp_reflp[OF a] equivp_reflp[OF b]) -apply(simp only: equivp_symp[OF a]) -apply(simp only: equivp_symp[OF b]) -using equivp_transp[OF a] apply blast -using equivp_transp[OF b] apply blast -done - -lemma prod_quotient: - assumes q1: "Quotient R1 Abs1 Rep1" - assumes q2: "Quotient R2 Abs2 Rep2" - shows "Quotient (prod_rel R1 R2) (prod_fun Abs1 Abs2) (prod_fun Rep1 Rep2)" -unfolding Quotient_def -apply (simp add: Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2] Quotient_rel_rep[OF q1] Quotient_rel_rep[OF q2]) -using Quotient_rel[OF q1] Quotient_rel[OF q2] by blast - -lemma pair_rsp: - assumes q1: "Quotient R1 Abs1 Rep1" - assumes q2: "Quotient R2 Abs2 Rep2" - shows "(R1 ===> R2 ===> prod_rel R1 R2) Pair Pair" -by auto - -lemma pair_prs: - assumes q1: "Quotient R1 Abs1 Rep1" - assumes q2: "Quotient R2 Abs2 Rep2" - shows "(prod_fun Abs1 Abs2) (Rep1 l, Rep2 r) \ (l, r)" - by (simp add: Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]) - -(* TODO: Is the quotient assumption q1 necessary? *) -(* TODO: Aren't there hard to use later? *) -lemma fst_rsp: - assumes q1: "Quotient R1 Abs1 Rep1" - assumes q2: "Quotient R2 Abs2 Rep2" - assumes a: "(prod_rel R1 R2) p1 p2" - shows "R1 (fst p1) (fst p2)" - using a - apply(case_tac p1) - apply(case_tac p2) - apply(auto) - done - -lemma snd_rsp: - assumes q1: "Quotient R1 Abs1 Rep1" - assumes q2: "Quotient R2 Abs2 Rep2" - assumes a: "(prod_rel R1 R2) p1 p2" - shows "R2 (snd p1) (snd p2)" - using a - apply(case_tac p1) - apply(case_tac p2) - apply(auto) - done - -lemma fst_prs: - assumes q1: "Quotient R1 Abs1 Rep1" - assumes q2: "Quotient R2 Abs2 Rep2" - shows "Abs1 (fst ((prod_fun Rep1 Rep2) p)) = fst p" -by (case_tac p) (auto simp add: Quotient_abs_rep[OF q1]) - -lemma snd_prs: - assumes q1: "Quotient R1 Abs1 Rep1" - assumes q2: "Quotient R2 Abs2 Rep2" - shows "Abs2 (snd ((prod_fun Rep1 Rep2) p)) = snd p" -by (case_tac p) (auto simp add: Quotient_abs_rep[OF q2]) - -end diff -r 6088fea1c8b1 -r 8a1c8dc72b5c QuotScript.thy --- a/QuotScript.thy Mon Dec 07 14:00:36 2009 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,569 +0,0 @@ -theory QuotScript -imports Plain ATP_Linkup -begin - -definition - "equivp E \ \x y. E x y = (E x = E y)" - -definition - "reflp E \ \x. E x x" - -definition - "symp E \ \x y. E x y \ E y x" - -definition - "transp E \ \x y z. E x y \ E y z \ E x z" - -lemma equivp_reflp_symp_transp: - shows "equivp E = (reflp E \ symp E \ transp E)" - unfolding equivp_def reflp_def symp_def transp_def expand_fun_eq - by (blast) - -lemma equivp_reflp: - shows "equivp E \ (\x. E x x)" - by (simp only: equivp_reflp_symp_transp reflp_def) - -lemma equivp_symp: - shows "equivp E \ (\x y. E x y \ E y x)" - by (metis equivp_reflp_symp_transp symp_def) - -lemma equivp_transp: - shows "equivp E \ (\x y z. E x y \ E y z \ E x z)" -by (metis equivp_reflp_symp_transp transp_def) - -definition - "part_equivp E \ (\x. E x x) \ (\x y. E x y = (E x x \ E y y \ (E x = E y)))" - -lemma equivp_IMP_part_equivp: - assumes a: "equivp E" - shows "part_equivp E" - using a unfolding equivp_def part_equivp_def - by auto - -definition - "Quotient E Abs Rep \ (\a. Abs (Rep a) = a) \ - (\a. E (Rep a) (Rep a)) \ - (\r s. E r s = (E r r \ E s s \ (Abs r = Abs s)))" - -lemma Quotient_abs_rep: - assumes a: "Quotient E Abs Rep" - shows "Abs (Rep a) \ a" - using a unfolding Quotient_def - by simp - -lemma Quotient_rep_reflp: - assumes a: "Quotient E Abs Rep" - shows "E (Rep a) (Rep a)" - using a unfolding Quotient_def - by blast - -lemma Quotient_rel: - assumes a: "Quotient E Abs Rep" - shows " E r s = (E r r \ E s s \ (Abs r = Abs s))" - using a unfolding Quotient_def - by blast - -lemma Quotient_rel_rep: - assumes a: "Quotient R Abs Rep" - shows "R (Rep a) (Rep b) \ (a = b)" - apply (rule eq_reflection) - using a unfolding Quotient_def - by metis - -lemma Quotient_rep_abs: - assumes a: "Quotient R Abs Rep" - shows "R r r \ R (Rep (Abs r)) r" - using a unfolding Quotient_def - by blast - -lemma identity_equivp: - shows "equivp (op =)" - unfolding equivp_def - by auto - -lemma identity_quotient: - shows "Quotient (op =) id id" - unfolding Quotient_def id_def - by blast - -lemma Quotient_symp: - assumes a: "Quotient E Abs Rep" - shows "symp E" - using a unfolding Quotient_def symp_def - by metis - -lemma Quotient_transp: - assumes a: "Quotient E Abs Rep" - shows "transp E" - using a unfolding Quotient_def transp_def - by metis - -fun - fun_map -where - "fun_map f g h x = g (h (f x))" - -abbreviation - fun_map_syn (infixr "--->" 55) -where - "f ---> g \ fun_map f g" - -lemma fun_map_id: - shows "(id ---> id) = id" - by (simp add: expand_fun_eq id_def) - -fun - fun_rel -where - "fun_rel E1 E2 f g = (\x y. E1 x y \ E2 (f x) (g y))" - -abbreviation - fun_rel_syn (infixr "===>" 55) -where - "E1 ===> E2 \ fun_rel E1 E2" - -lemma fun_rel_eq: - "(op =) ===> (op =) \ (op =)" -by (rule eq_reflection) (simp add: expand_fun_eq) - -lemma fun_quotient: - assumes q1: "Quotient R1 abs1 rep1" - and q2: "Quotient R2 abs2 rep2" - shows "Quotient (R1 ===> R2) (rep1 ---> abs2) (abs1 ---> rep2)" -proof - - have "\a. (rep1 ---> abs2) ((abs1 ---> rep2) a) = a" - apply(simp add: expand_fun_eq) - using q1 q2 - apply(simp add: Quotient_def) - done - moreover - have "\a. (R1 ===> R2) ((abs1 ---> rep2) a) ((abs1 ---> rep2) a)" - apply(auto) - using q1 q2 unfolding Quotient_def - apply(metis) - done - moreover - have "\r s. (R1 ===> R2) r s = ((R1 ===> R2) r r \ (R1 ===> R2) s s \ - (rep1 ---> abs2) r = (rep1 ---> abs2) s)" - apply(auto simp add: expand_fun_eq) - using q1 q2 unfolding Quotient_def - apply(metis) - using q1 q2 unfolding Quotient_def - apply(metis) - using q1 q2 unfolding Quotient_def - apply(metis) - using q1 q2 unfolding Quotient_def - apply(metis) - done - ultimately - show "Quotient (R1 ===> R2) (rep1 ---> abs2) (abs1 ---> rep2)" - unfolding Quotient_def by blast -qed - -definition - Respects -where - "Respects R x \ (R x x)" - -lemma in_respects: - shows "(x \ Respects R) = R x x" - unfolding mem_def Respects_def by simp - -lemma equals_rsp: - assumes q: "Quotient R Abs Rep" - and a: "R xa xb" "R ya yb" - shows "R xa ya = R xb yb" - using Quotient_symp[OF q] Quotient_transp[OF q] unfolding symp_def transp_def - using a by blast - -lemma lambda_prs: - assumes q1: "Quotient R1 Abs1 Rep1" - and q2: "Quotient R2 Abs2 Rep2" - shows "(Rep1 ---> Abs2) (\x. Rep2 (f (Abs1 x))) = (\x. f x)" - unfolding expand_fun_eq - using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2] - by simp - -lemma lambda_prs1: - assumes q1: "Quotient R1 Abs1 Rep1" - and q2: "Quotient R2 Abs2 Rep2" - shows "(Rep1 ---> Abs2) (\x. (Abs1 ---> Rep2) f x) = (\x. f x)" - unfolding expand_fun_eq - using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2] - by simp - -lemma rep_abs_rsp: - assumes q: "Quotient R Abs Rep" - and a: "R x1 x2" - shows "R x1 (Rep (Abs x2))" - using q a by (metis Quotient_rel[OF q] Quotient_abs_rep[OF q] Quotient_rep_reflp[OF q]) - -(* In the following theorem R1 can be instantiated with anything, - but we know some of the types of the Rep and Abs functions; - so by solving Quotient assumptions we can get a unique R1 that - will be provable; which is why we need to use apply_rsp and - not the primed version *) -lemma apply_rsp: - assumes q: "Quotient R1 Abs1 Rep1" - and a: "(R1 ===> R2) f g" "R1 x y" - shows "R2 ((f::'a\'c) x) ((g::'a\'c) y)" - using a by simp - -lemma apply_rsp': - assumes a: "(R1 ===> R2) f g" "R1 x y" - shows "R2 (f x) (g y)" - using a by simp - -(* Set of lemmas for regularisation of ball and bex *) - -lemma ball_reg_eqv: - fixes P :: "'a \ bool" - assumes a: "equivp R" - shows "Ball (Respects R) P = (All P)" - by (metis equivp_def in_respects a) - -lemma bex_reg_eqv: - fixes P :: "'a \ bool" - assumes a: "equivp R" - shows "Bex (Respects R) P = (Ex P)" - by (metis equivp_def in_respects a) - -lemma ball_reg_right: - assumes a: "\x. R x \ P x \ Q x" - shows "All P \ Ball R Q" - by (metis COMBC_def Collect_def Collect_mem_eq a) - -lemma bex_reg_left: - assumes a: "\x. R x \ Q x \ P x" - shows "Bex R Q \ Ex P" - by (metis COMBC_def Collect_def Collect_mem_eq a) - -lemma ball_reg_left: - assumes a: "equivp R" - shows "(\x. (Q x \ P x)) \ Ball (Respects R) Q \ All P" - by (metis equivp_reflp in_respects a) - -lemma bex_reg_right: - assumes a: "equivp R" - shows "(\x. (Q x \ P x)) \ Ex Q \ Bex (Respects R) P" - by (metis equivp_reflp in_respects a) - -lemma ball_reg_eqv_range: - fixes P::"'a \ bool" - and x::"'a" - assumes a: "equivp R2" - shows "(Ball (Respects (R1 ===> R2)) (\f. P (f x)) = All (\f. P (f x)))" - apply(rule iffI) - apply(rule allI) - apply(drule_tac x="\y. f x" in bspec) - apply(simp add: Respects_def in_respects) - apply(rule impI) - using a equivp_reflp_symp_transp[of "R2"] - apply(simp add: reflp_def) - apply(simp) - apply(simp) - done - -lemma bex_reg_eqv_range: - fixes P::"'a \ bool" - and x::"'a" - assumes a: "equivp R2" - shows "(Bex (Respects (R1 ===> R2)) (\f. P (f x)) = Ex (\f. P (f x)))" - apply(auto) - apply(rule_tac x="\y. f x" in bexI) - apply(simp) - apply(simp add: Respects_def in_respects) - apply(rule impI) - using a equivp_reflp_symp_transp[of "R2"] - apply(simp add: reflp_def) - done - -lemma all_reg: - assumes a: "!x :: 'a. (P x --> Q x)" - and b: "All P" - shows "All Q" - using a b by (metis) - -lemma ex_reg: - assumes a: "!x :: 'a. (P x --> Q x)" - and b: "Ex P" - shows "Ex Q" - using a b by (metis) - -lemma ball_reg: - assumes a: "!x :: 'a. (R x --> P x --> Q x)" - and b: "Ball R P" - shows "Ball R Q" - using a b by (metis COMBC_def Collect_def Collect_mem_eq) - -lemma bex_reg: - assumes a: "!x :: 'a. (R x --> P x --> Q x)" - and b: "Bex R P" - shows "Bex R Q" - using a b by (metis COMBC_def Collect_def Collect_mem_eq) - -lemma ball_all_comm: - "(\y. (\x\P. A x y) \ (\x. B x y)) \ ((\x\P. \y. A x y) \ (\x. \y. B x y))" -by auto - -lemma bex_ex_comm: - "((\y. \x. A x y) \ (\y. \x\P. B x y)) \ ((\x. \y. A x y) \ (\x\P. \y. B x y))" -by auto - -(* Bounded abstraction *) -definition - Babs :: "('a \ bool) \ ('a \ 'b) \ 'a \ 'b" -where - "(x \ p) \ (Babs p m x = m x)" - -(* 3 lemmas needed for proving repabs_inj *) -lemma ball_rsp: - assumes a: "(R ===> (op =)) f g" - shows "Ball (Respects R) f = Ball (Respects R) g" - using a by (simp add: Ball_def in_respects) - -lemma bex_rsp: - assumes a: "(R ===> (op =)) f g" - shows "(Bex (Respects R) f = Bex (Respects R) g)" - using a by (simp add: Bex_def in_respects) - -lemma babs_rsp: - assumes q: "Quotient R1 Abs1 Rep1" - and a: "(R1 ===> R2) f g" - shows "(R1 ===> R2) (Babs (Respects R1) f) (Babs (Respects R1) g)" - apply (auto simp add: Babs_def) - apply (subgoal_tac "x \ Respects R1 \ y \ Respects R1") - using a apply (simp add: Babs_def) - apply (simp add: in_respects) - using Quotient_rel[OF q] - by metis - -(* 2 lemmas needed for cleaning of quantifiers *) -lemma all_prs: - assumes a: "Quotient R absf repf" - shows "Ball (Respects R) ((absf ---> id) f) = All f" - using a unfolding Quotient_def - by (metis in_respects fun_map.simps id_apply) - -lemma ex_prs: - assumes a: "Quotient R absf repf" - shows "Bex (Respects R) ((absf ---> id) f) = Ex f" - using a unfolding Quotient_def - by (metis COMBC_def Collect_def Collect_mem_eq in_respects fun_map.simps id_apply) - -lemma fun_rel_id: - assumes a: "\x y. R1 x y \ R2 (f x) (g y)" - shows "(R1 ===> R2) f g" -using a by simp - -lemma quot_rel_rsp: - assumes a: "Quotient R Abs Rep" - shows "(R ===> R ===> op =) R R" - apply(rule fun_rel_id)+ - apply(rule equals_rsp[OF a]) - apply(assumption)+ - done - - - - - - -(******************************************) -(* REST OF THE FILE IS UNUSED (until now) *) -(******************************************) -lemma Quotient_rel_abs: - assumes a: "Quotient E Abs Rep" - shows "E r s \ Abs r = Abs s" -using a unfolding Quotient_def -by blast - -lemma Quotient_rel_abs_eq: - assumes a: "Quotient E Abs Rep" - shows "E r r \ E s s \ E r s = (Abs r = Abs s)" -using a unfolding Quotient_def -by blast - -lemma in_fun: - shows "x \ ((f ---> g) s) = g (f x \ s)" -by (simp add: mem_def) - -lemma RESPECTS_THM: - shows "Respects (R1 ===> R2) f = (\x y. R1 x y \ R2 (f x) (f y))" -unfolding Respects_def -by (simp add: expand_fun_eq) - -lemma RESPECTS_REP_ABS: - assumes a: "Quotient R1 Abs1 Rep1" - and b: "Respects (R1 ===> R2) f" - and c: "R1 x x" - shows "R2 (f (Rep1 (Abs1 x))) (f x)" -using a b[simplified RESPECTS_THM] c unfolding Quotient_def -by blast - -lemma RESPECTS_MP: - assumes a: "Respects (R1 ===> R2) f" - and b: "R1 x y" - shows "R2 (f x) (f y)" -using a b unfolding Respects_def -by simp - -lemma RESPECTS_o: - assumes a: "Respects (R2 ===> R3) f" - and b: "Respects (R1 ===> R2) g" - shows "Respects (R1 ===> R3) (f o g)" -using a b unfolding Respects_def -by simp - -lemma fun_rel_EQ_REL: - assumes q1: "Quotient R1 Abs1 Rep1" - and q2: "Quotient R2 Abs2 Rep2" - shows "(R1 ===> R2) f g = ((Respects (R1 ===> R2) f) \ (Respects (R1 ===> R2) g) - \ ((Rep1 ---> Abs2) f = (Rep1 ---> Abs2) g))" -using fun_quotient[OF q1 q2] unfolding Respects_def Quotient_def expand_fun_eq -by blast - -(* Not used since in the end we just unfold fun_map *) -lemma APP_PRS: - assumes q1: "Quotient R1 abs1 rep1" - and q2: "Quotient R2 abs2 rep2" - shows "abs2 ((abs1 ---> rep2) f (rep1 x)) = f x" -unfolding expand_fun_eq -using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2] -by simp - -(* Ask Peter: assumption q1 and q2 not used and lemma is the 'identity' *) -lemma LAMBDA_RSP: - assumes q1: "Quotient R1 Abs1 Rep1" - and q2: "Quotient R2 Abs2 Rep2" - and a: "(R1 ===> R2) f1 f2" - shows "(R1 ===> R2) (\x. f1 x) (\y. f2 y)" -by (rule a) - -(* ASK Peter about next four lemmas in quotientScript -lemma ABSTRACT_PRS: - assumes q1: "Quotient R1 Abs1 Rep1" - and q2: "Quotient R2 Abs2 Rep2" - shows "f = (Rep1 ---> Abs2) ???" -*) - - -lemma fun_rel_EQUALS: - assumes q1: "Quotient R1 Abs1 Rep1" - and q2: "Quotient R2 Abs2 Rep2" - and r1: "Respects (R1 ===> R2) f" - and r2: "Respects (R1 ===> R2) g" - shows "((Rep1 ---> Abs2) f = (Rep1 ---> Abs2) g) = (\x y. R1 x y \ R2 (f x) (g y))" -apply(rule_tac iffI) -using fun_quotient[OF q1 q2] r1 r2 unfolding Quotient_def Respects_def -apply(metis apply_rsp') -using r1 unfolding Respects_def expand_fun_eq -apply(simp (no_asm_use)) -apply(metis Quotient_rel[OF q2] Quotient_rel_rep[OF q1]) -done - -(* ask Peter: fun_rel_IMP used twice *) -lemma fun_rel_IMP2: - assumes q1: "Quotient R1 Abs1 Rep1" - and q2: "Quotient R2 Abs2 Rep2" - and r1: "Respects (R1 ===> R2) f" - and r2: "Respects (R1 ===> R2) g" - and a: "(Rep1 ---> Abs2) f = (Rep1 ---> Abs2) g" - shows "R1 x y \ R2 (f x) (g y)" -using q1 q2 r1 r2 a -by (simp add: fun_rel_EQUALS) - -lemma LAMBDA_REP_ABS_RSP: - assumes r1: "\r r'. R1 r r' \R1 r (Rep1 (Abs1 r'))" - and r2: "\r r'. R2 r r' \R2 r (Rep2 (Abs2 r'))" - shows "(R1 ===> R2) f1 f2 \ (R1 ===> R2) f1 ((Abs1 ---> Rep2) ((Rep1 ---> Abs2) f2))" -using r1 r2 by auto - -(* Not used *) -lemma rep_abs_rsp_left: - assumes q: "Quotient R Abs Rep" - and a: "R x1 x2" - shows "R x1 (Rep (Abs x2))" -using q a by (metis Quotient_rel[OF q] Quotient_abs_rep[OF q] Quotient_rep_reflp[OF q]) - - - -(* bool theory: COND, LET *) -lemma IF_PRS: - assumes q: "Quotient R Abs Rep" - shows "If a b c = Abs (If a (Rep b) (Rep c))" -using Quotient_abs_rep[OF q] by auto - -(* ask peter: no use of q *) -lemma IF_RSP: - assumes q: "Quotient R Abs Rep" - and a: "a1 = a2" "R b1 b2" "R c1 c2" - shows "R (If a1 b1 c1) (If a2 b2 c2)" -using a by auto - -lemma LET_PRS: - assumes q1: "Quotient R1 Abs1 Rep1" - and q2: "Quotient R2 Abs2 Rep2" - shows "Let x f = Abs2 (Let (Rep1 x) ((Abs1 ---> Rep2) f))" -using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2] by auto - -lemma LET_RSP: - assumes q1: "Quotient R1 Abs1 Rep1" - and a1: "(R1 ===> R2) f g" - and a2: "R1 x y" - shows "R2 ((Let x f)::'c) ((Let y g)::'c)" -using apply_rsp[OF q1 a1] a2 -by auto - - - -(* ask peter what are literal_case *) -(* literal_case_PRS *) -(* literal_case_RSP *) - - - - - -(* combinators: I, K, o, C, W *) - -(* We use id_simps which includes id_apply; so these 2 theorems can be removed *) - -lemma I_PRS: - assumes q: "Quotient R Abs Rep" - shows "id e = Abs (id (Rep e))" -using Quotient_abs_rep[OF q] by auto - -lemma I_RSP: - assumes q: "Quotient R Abs Rep" - and a: "R e1 e2" - shows "R (id e1) (id e2)" -using a by auto - -lemma o_PRS: - assumes q1: "Quotient R1 Abs1 Rep1" - and q2: "Quotient R2 Abs2 Rep2" - and q3: "Quotient R3 Abs3 Rep3" - shows "f o g = (Rep1 ---> Abs3) (((Abs2 ---> Rep3) f) o ((Abs1 ---> Rep2) g))" -using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2] Quotient_abs_rep[OF q3] -unfolding o_def expand_fun_eq -by simp - -lemma o_RSP: - assumes q1: "Quotient R1 Abs1 Rep1" - and q2: "Quotient R2 Abs2 Rep2" - and q3: "Quotient R3 Abs3 Rep3" - and a1: "(R2 ===> R3) f1 f2" - and a2: "(R1 ===> R2) g1 g2" - shows "(R1 ===> R3) (f1 o g1) (f2 o g2)" -using a1 a2 unfolding o_def expand_fun_eq -by (auto) - -lemma COND_PRS: - assumes a: "Quotient R absf repf" - shows "(if a then b else c) = absf (if a then repf b else repf c)" - using a unfolding Quotient_def by auto - - -end - diff -r 6088fea1c8b1 -r 8a1c8dc72b5c Quotients.thy --- a/Quotients.thy Mon Dec 07 14:00:36 2009 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,80 +0,0 @@ -theory Quotients -imports Main -begin - -(* Other quotients that have not been proved yet *) - -fun - option_rel -where - "option_rel R None None = True" -| "option_rel R (Some x) None = False" -| "option_rel R None (Some x) = False" -| "option_rel R (Some x) (Some y) = R x y" - -fun - option_map -where - "option_map f None = None" -| "option_map f (Some x) = Some (f x)" - -fun - prod_rel -where - "prod_rel R1 R2 (a1,a2) (b1,b2) = (R1 a1 b1 \ R2 a2 b2)" - -fun - prod_map -where - "prod_map f1 f2 (a,b) = (f1 a, f2 b)" - -fun - sum_rel -where - "sum_rel R1 R2 (Inl a1) (Inl b1) = R1 a1 b1" -| "sum_rel R1 R2 (Inl a1) (Inr b2) = False" -| "sum_rel R1 R2 (Inr a2) (Inl b1) = False" -| "sum_rel R1 R2 (Inr a2) (Inr b2) = R2 a2 b2" - -fun - sum_map -where - "sum_map f1 f2 (Inl a) = Inl (f1 a)" -| "sum_map f1 f2 (Inr a) = Inr (f2 a)" - - - - - -fun - noption_map::"('a \ 'b) \ ('a noption) \ ('b noption)" -where - "noption_map f (nSome x) = nSome (f x)" -| "noption_map f nNone = nNone" - -fun - noption_rel -where - "noption_rel r (nSome x) (nSome y) = r x y" -| "noption_rel r _ _ = False" - -declare [[map noption = (noption_map, noption_rel)]] - -lemma "noption_map id = id" -sorry - -lemma noption_Quotient: - assumes q: "Quotient R Abs Rep" - shows "Quotient (noption_rel R) (noption_map Abs) (noption_map Rep)" - apply (unfold Quotient_def) - apply (auto) - using q - apply (unfold Quotient_def) - apply (case_tac "a :: 'b noption") - apply (simp) - apply (simp) - apply (case_tac "a :: 'b noption") - apply (simp only: option_map.simps) - apply (subst option_rel.simps) - (* Simp starts hanging so don't know how to continue *) - sorry