# HG changeset patch # User haftmann # Date 1248188538 -7200 # Node ID 631546213601570e25605337d01d73c1cae8375c # Parent 6da9c2a49fed6edc61a9f74c5a2e5337f66eb615# Parent a5042f26044076bc2aa710cb7185f9527733ca38 merged diff -r 6da9c2a49fed -r 631546213601 src/HOL/Auth/Message.thy --- a/src/HOL/Auth/Message.thy Tue Jul 21 14:08:58 2009 +0200 +++ b/src/HOL/Auth/Message.thy Tue Jul 21 17:02:18 2009 +0200 @@ -856,6 +856,8 @@ Abstraction over i is ESSENTIAL: it delays the dereferencing of claset DEPENDS UPON "X" REFERRING TO THE FRADULENT MESSAGE *) +fun impOfSubs th = th RSN (2, @{thm rev_subsetD}) + (*Apply rules to break down assumptions of the form Y \ parts(insert X H) and Y \ analz(insert X H) *) diff -r 6da9c2a49fed -r 631546213601 src/HOL/HOL.thy --- a/src/HOL/HOL.thy Tue Jul 21 14:08:58 2009 +0200 +++ b/src/HOL/HOL.thy Tue Jul 21 17:02:18 2009 +0200 @@ -107,7 +107,6 @@ notation (xsymbols) iff (infixr "\" 25) - nonterminals letbinds letbind case_syn cases_syn @@ -198,96 +197,9 @@ axiomatization undefined :: 'a - -subsubsection {* Generic classes and algebraic operations *} - class default = fixes default :: 'a -class zero = - fixes zero :: 'a ("0") - -class one = - fixes one :: 'a ("1") - -hide (open) const zero one - -class plus = - fixes plus :: "'a \ 'a \ 'a" (infixl "+" 65) - -class minus = - fixes minus :: "'a \ 'a \ 'a" (infixl "-" 65) - -class uminus = - fixes uminus :: "'a \ 'a" ("- _" [81] 80) - -class times = - fixes times :: "'a \ 'a \ 'a" (infixl "*" 70) - -class inverse = - fixes inverse :: "'a \ 'a" - and divide :: "'a \ 'a \ 'a" (infixl "'/" 70) - -class abs = - fixes abs :: "'a \ 'a" -begin - -notation (xsymbols) - abs ("\_\") - -notation (HTML output) - abs ("\_\") - -end - -class sgn = - fixes sgn :: "'a \ 'a" - -class ord = - fixes less_eq :: "'a \ 'a \ bool" - and less :: "'a \ 'a \ bool" -begin - -notation - less_eq ("op <=") and - less_eq ("(_/ <= _)" [51, 51] 50) and - less ("op <") and - less ("(_/ < _)" [51, 51] 50) - -notation (xsymbols) - less_eq ("op \") and - less_eq ("(_/ \ _)" [51, 51] 50) - -notation (HTML output) - less_eq ("op \") and - less_eq ("(_/ \ _)" [51, 51] 50) - -abbreviation (input) - greater_eq (infix ">=" 50) where - "x >= y \ y <= x" - -notation (input) - greater_eq (infix "\" 50) - -abbreviation (input) - greater (infix ">" 50) where - "x > y \ y < x" - -end - -syntax - "_index1" :: index ("\<^sub>1") -translations - (index) "\<^sub>1" => (index) "\<^bsub>\\<^esub>" - -typed_print_translation {* -let - fun tr' c = (c, fn show_sorts => fn T => fn ts => - if (not o null) ts orelse T = dummyT orelse not (! show_types) andalso can Term.dest_Type T then raise Match - else Syntax.const Syntax.constrainC $ Syntax.const c $ Syntax.term_of_typ show_sorts T); -in map tr' [@{const_syntax HOL.one}, @{const_syntax HOL.zero}] end; -*} -- {* show types that are presumably too general *} - subsection {* Fundamental rules *} @@ -1605,25 +1517,9 @@ setup ReorientProc.init -setup {* - ReorientProc.add - (fn Const(@{const_name HOL.zero}, _) => true - | Const(@{const_name HOL.one}, _) => true - | _ => false) -*} - -simproc_setup reorient_zero ("0 = x") = ReorientProc.proc -simproc_setup reorient_one ("1 = x") = ReorientProc.proc - subsection {* Other simple lemmas and lemma duplicates *} -lemma Let_0 [simp]: "Let 0 f = f 0" - unfolding Let_def .. - -lemma Let_1 [simp]: "Let 1 f = f 1" - unfolding Let_def .. - lemma ex1_eq [iff]: "EX! x. x = t" "EX! x. t = x" by blast+ @@ -1643,13 +1539,6 @@ apply (drule_tac [3] x = x in fun_cong, simp_all) done -lemma mk_left_commute: - fixes f (infix "\" 60) - assumes a: "\x y z. (x \ y) \ z = x \ (y \ z)" and - c: "\x y. x \ y = y \ x" - shows "x \ (y \ z) = y \ (x \ z)" - by (rule trans [OF trans [OF c a] arg_cong [OF c, of "f y"]]) - lemmas eq_sym_conv = eq_commute lemma nnf_simps: @@ -1659,6 +1548,118 @@ by blast+ +subsection {* Generic classes and algebraic operations *} + +class zero = + fixes zero :: 'a ("0") + +class one = + fixes one :: 'a ("1") + +lemma Let_0 [simp]: "Let 0 f = f 0" + unfolding Let_def .. + +lemma Let_1 [simp]: "Let 1 f = f 1" + unfolding Let_def .. + +setup {* + ReorientProc.add + (fn Const(@{const_name HOL.zero}, _) => true + | Const(@{const_name HOL.one}, _) => true + | _ => false) +*} + +simproc_setup reorient_zero ("0 = x") = ReorientProc.proc +simproc_setup reorient_one ("1 = x") = ReorientProc.proc + +typed_print_translation {* +let + fun tr' c = (c, fn show_sorts => fn T => fn ts => + if (not o null) ts orelse T = dummyT + orelse not (! show_types) andalso can Term.dest_Type T + then raise Match + else Syntax.const Syntax.constrainC $ Syntax.const c $ Syntax.term_of_typ show_sorts T); +in map tr' [@{const_syntax HOL.one}, @{const_syntax HOL.zero}] end; +*} -- {* show types that are presumably too general *} + +hide (open) const zero one + +class plus = + fixes plus :: "'a \ 'a \ 'a" (infixl "+" 65) + +class minus = + fixes minus :: "'a \ 'a \ 'a" (infixl "-" 65) + +class uminus = + fixes uminus :: "'a \ 'a" ("- _" [81] 80) + +class times = + fixes times :: "'a \ 'a \ 'a" (infixl "*" 70) + +class inverse = + fixes inverse :: "'a \ 'a" + and divide :: "'a \ 'a \ 'a" (infixl "'/" 70) + +class abs = + fixes abs :: "'a \ 'a" +begin + +notation (xsymbols) + abs ("\_\") + +notation (HTML output) + abs ("\_\") + +end + +class sgn = + fixes sgn :: "'a \ 'a" + +class ord = + fixes less_eq :: "'a \ 'a \ bool" + and less :: "'a \ 'a \ bool" +begin + +notation + less_eq ("op <=") and + less_eq ("(_/ <= _)" [51, 51] 50) and + less ("op <") and + less ("(_/ < _)" [51, 51] 50) + +notation (xsymbols) + less_eq ("op \") and + less_eq ("(_/ \ _)" [51, 51] 50) + +notation (HTML output) + less_eq ("op \") and + less_eq ("(_/ \ _)" [51, 51] 50) + +abbreviation (input) + greater_eq (infix ">=" 50) where + "x >= y \ y <= x" + +notation (input) + greater_eq (infix "\" 50) + +abbreviation (input) + greater (infix ">" 50) where + "x > y \ y < x" + +end + +syntax + "_index1" :: index ("\<^sub>1") +translations + (index) "\<^sub>1" => (index) "\<^bsub>\\<^esub>" + +lemma mk_left_commute: + fixes f (infix "\" 60) + assumes a: "\x y z. (x \ y) \ z = x \ (y \ z)" and + c: "\x y. x \ y = y \ x" + shows "x \ (y \ z) = y \ (x \ z)" + by (rule trans [OF trans [OF c a] arg_cong [OF c, of "f y"]]) + + subsection {* Basic ML bindings *} ML {* diff -r 6da9c2a49fed -r 631546213601 src/HOL/NatTransfer.thy --- a/src/HOL/NatTransfer.thy Tue Jul 21 14:08:58 2009 +0200 +++ b/src/HOL/NatTransfer.thy Tue Jul 21 17:02:18 2009 +0200 @@ -380,12 +380,16 @@ "(even (int x)) = (even x)" by (auto simp add: zdvd_int even_nat_def) +lemma UNIV_apply: + "UNIV x = True" + by (simp add: top_set_eq [symmetric] top_fun_eq top_bool_eq) + declare TransferMorphism_int_nat[transfer add return: transfer_int_nat_numerals transfer_int_nat_functions transfer_int_nat_function_closures transfer_int_nat_relations - UNIV_code + UNIV_apply ] diff -r 6da9c2a49fed -r 631546213601 src/HOL/Nominal/nominal_datatype.ML --- a/src/HOL/Nominal/nominal_datatype.ML Tue Jul 21 14:08:58 2009 +0200 +++ b/src/HOL/Nominal/nominal_datatype.ML Tue Jul 21 17:02:18 2009 +0200 @@ -815,7 +815,7 @@ val (thy', defs', eqns') = Library.foldl (make_constr_def tname T T') ((Sign.add_path tname thy, defs, []), constrs ~~ constrs' ~~ constr_syntax) in - (parent_path (#flat_names config) thy', defs', eqns @ [eqns'], dist_lemmas @ [dist]) + (Sign.parent_path thy', defs', eqns @ [eqns'], dist_lemmas @ [dist]) end; val (thy8, constr_defs, constr_rep_eqns, dist_lemmas) = Library.foldl dt_constr_defs diff -r 6da9c2a49fed -r 631546213601 src/HOL/PReal.thy --- a/src/HOL/PReal.thy Tue Jul 21 14:08:58 2009 +0200 +++ b/src/HOL/PReal.thy Tue Jul 21 17:02:18 2009 +0200 @@ -52,7 +52,7 @@ definition psup :: "preal set => preal" where - "psup P = Abs_preal (\X \ P. Rep_preal X)" + [code del]: "psup P = Abs_preal (\X \ P. Rep_preal X)" definition add_set :: "[rat set,rat set] => rat set" where diff -r 6da9c2a49fed -r 631546213601 src/HOL/SET-Protocol/MessageSET.thy --- a/src/HOL/SET-Protocol/MessageSET.thy Tue Jul 21 14:08:58 2009 +0200 +++ b/src/HOL/SET-Protocol/MessageSET.thy Tue Jul 21 17:02:18 2009 +0200 @@ -854,6 +854,8 @@ Abstraction over i is ESSENTIAL: it delays the dereferencing of claset DEPENDS UPON "X" REFERRING TO THE FRADULENT MESSAGE *) +fun impOfSubs th = th RSN (2, @{thm rev_subsetD}) + (*Apply rules to break down assumptions of the form Y \ parts(insert X H) and Y \ analz(insert X H) *) diff -r 6da9c2a49fed -r 631546213601 src/HOL/Set.thy --- a/src/HOL/Set.thy Tue Jul 21 14:08:58 2009 +0200 +++ b/src/HOL/Set.thy Tue Jul 21 17:02:18 2009 +0200 @@ -80,12 +80,30 @@ lemma Collect_cong: "(!!x. P x = Q x) ==> {x. P(x)} = {x. Q(x)}" by simp +text {* +Simproc for pulling @{text "x=t"} in @{text "{x. \ & x=t & \}"} +to the front (and similarly for @{text "t=x"}): +*} + +setup {* +let + val Coll_perm_tac = rtac @{thm Collect_cong} 1 THEN rtac @{thm iffI} 1 THEN + ALLGOALS(EVERY'[REPEAT_DETERM o (etac @{thm conjE}), + DEPTH_SOLVE_1 o (ares_tac [@{thm conjI}])]) + val defColl_regroup = Simplifier.simproc @{theory} + "defined Collect" ["{x. P x & Q x}"] + (Quantifier1.rearrange_Coll Coll_perm_tac) +in + Simplifier.map_simpset (fn ss => ss addsimprocs [defColl_regroup]) +end +*} + lemmas CollectE = CollectD [elim_format] text {* Set enumerations *} definition empty :: "'a set" ("{}") where - "empty \ {x. False}" + "empty = {x. False}" definition insert :: "'a \ 'a set \ 'a set" where insert_compr: "insert a B = {x. x = a \ x \ B}" @@ -273,14 +291,10 @@ in [("@SetCompr", setcompr_tr)] end; *} -(* To avoid eta-contraction of body: *) -print_translation {* -let - fun btr' syn [A, Abs abs] = - let val (x, t) = atomic_abs_tr' abs - in Syntax.const syn $ x $ A $ t end -in [(@{const_syntax Ball}, btr' "_Ball"), (@{const_syntax Bex}, btr' "_Bex")] end -*} +print_translation {* [ +Syntax.preserve_binder_abs2_tr' @{const_syntax Ball} "_Ball", +Syntax.preserve_binder_abs2_tr' @{const_syntax Bex} "_Bex" +] *} -- {* to avoid eta-contraction of body *} print_translation {* let @@ -311,6 +325,23 @@ in [("Collect", setcompr_tr')] end; *} +setup {* +let + val unfold_bex_tac = unfold_tac @{thms "Bex_def"}; + fun prove_bex_tac ss = unfold_bex_tac ss THEN Quantifier1.prove_one_point_ex_tac; + val rearrange_bex = Quantifier1.rearrange_bex prove_bex_tac; + val unfold_ball_tac = unfold_tac @{thms "Ball_def"}; + fun prove_ball_tac ss = unfold_ball_tac ss THEN Quantifier1.prove_one_point_all_tac; + val rearrange_ball = Quantifier1.rearrange_ball prove_ball_tac; + val defBEX_regroup = Simplifier.simproc @{theory} + "defined BEX" ["EX x:A. P x & Q x"] rearrange_bex; + val defBALL_regroup = Simplifier.simproc @{theory} + "defined BALL" ["ALL x:A. P x --> Q x"] rearrange_ball; +in + Simplifier.map_simpset (fn ss => ss addsimprocs [defBALL_regroup, defBEX_regroup]) +end +*} + lemma ballI [intro!]: "(!!x. x:A ==> P x) ==> ALL x:A. P x" by (simp add: Ball_def) @@ -319,20 +350,6 @@ lemma bspec [dest?]: "ALL x:A. P x ==> x:A ==> P x" by (simp add: Ball_def) -lemma ballE [elim]: "ALL x:A. P x ==> (P x ==> Q) ==> (x ~: A ==> Q) ==> Q" - by (unfold Ball_def) blast - -ML {* bind_thm ("rev_ballE", Thm.permute_prems 1 1 @{thm ballE}) *} - -text {* - \medskip This tactic takes assumptions @{prop "ALL x:A. P x"} and - @{prop "a:A"}; creates assumption @{prop "P a"}. -*} - -ML {* - fun ball_tac i = etac @{thm ballE} i THEN contr_tac (i + 1) -*} - text {* Gives better instantiation for bound: *} @@ -341,6 +358,26 @@ Classical.map_cs (fn cs => cs addbefore ("bspec", datac @{thm bspec} 1)) *} +ML {* +structure Simpdata = +struct + +open Simpdata; + +val mksimps_pairs = [(@{const_name Ball}, @{thms bspec})] @ mksimps_pairs; + +end; + +open Simpdata; +*} + +declaration {* fn _ => + Simplifier.map_ss (fn ss => ss setmksimps (mksimps mksimps_pairs)) +*} + +lemma ballE [elim]: "ALL x:A. P x ==> (P x ==> Q) ==> (x ~: A ==> Q) ==> Q" + by (unfold Ball_def) blast + lemma bexI [intro]: "P x ==> x:A ==> EX x:A. P x" -- {* Normally the best argument order: @{prop "P x"} constrains the choice of @{prop "x:A"}. *} @@ -382,24 +419,6 @@ lemma ball_one_point2 [simp]: "(ALL x:A. a = x --> P x) = (a:A --> P a)" by blast -ML {* - local - val unfold_bex_tac = unfold_tac @{thms "Bex_def"}; - fun prove_bex_tac ss = unfold_bex_tac ss THEN Quantifier1.prove_one_point_ex_tac; - val rearrange_bex = Quantifier1.rearrange_bex prove_bex_tac; - - val unfold_ball_tac = unfold_tac @{thms "Ball_def"}; - fun prove_ball_tac ss = unfold_ball_tac ss THEN Quantifier1.prove_one_point_all_tac; - val rearrange_ball = Quantifier1.rearrange_ball prove_ball_tac; - in - val defBEX_regroup = Simplifier.simproc @{theory} - "defined BEX" ["EX x:A. P x & Q x"] rearrange_bex; - val defBALL_regroup = Simplifier.simproc @{theory} - "defined BALL" ["ALL x:A. P x --> Q x"] rearrange_ball; - end; - - Addsimprocs [defBALL_regroup, defBEX_regroup]; -*} text {* Congruence rules *} @@ -450,25 +469,12 @@ \medskip Converts @{prop "A \ B"} to @{prop "x \ A ==> x \ B"}. *} -ML {* - fun impOfSubs th = th RSN (2, @{thm rev_subsetD}) -*} - lemma subsetCE [elim]: "A \ B ==> (c \ A ==> P) ==> (c \ B ==> P) ==> P" -- {* Classical elimination rule. *} by (unfold mem_def) blast lemma subset_eq: "A \ B = (\x\A. x \ B)" by blast -text {* - \medskip Takes assumptions @{prop "A \ B"}; @{prop "c \ A"} and - creates the assumption @{prop "c \ B"}. -*} - -ML {* - fun set_mp_tac i = etac @{thm subsetCE} i THEN mp_tac i -*} - lemma contra_subsetD: "A \ B ==> c \ B ==> c \ A" by blast @@ -538,7 +544,7 @@ subsubsection {* The universal set -- UNIV *} definition UNIV :: "'a set" where - "UNIV \ {x. True}" + "UNIV = {x. True}" lemma UNIV_I [simp]: "x : UNIV" by (simp add: UNIV_def) @@ -647,7 +653,7 @@ subsubsection {* Binary union -- Un *} definition Un :: "'a set \ 'a set \ 'a set" (infixl "Un" 65) where - "A Un B \ {x. x \ A \ x \ B}" + "A Un B = {x. x \ A \ x \ B}" notation (xsymbols) "Un" (infixl "\" 65) @@ -678,7 +684,7 @@ lemma UnE [elim!]: "c : A Un B ==> (c:A ==> P) ==> (c:B ==> P) ==> P" by (unfold Un_def) blast -lemma insert_def: "insert a B \ {x. x = a} \ B" +lemma insert_def: "insert a B = {x. x = a} \ B" by (simp add: Collect_def mem_def insert_compr Un_def) lemma mono_Un: "mono f \ f A \ f B \ f (A \ B)" @@ -690,7 +696,7 @@ subsubsection {* Binary intersection -- Int *} definition Int :: "'a set \ 'a set \ 'a set" (infixl "Int" 70) where - "A Int B \ {x. x \ A \ x \ B}" + "A Int B = {x. x \ A \ x \ B}" notation (xsymbols) "Int" (infixl "\" 70) @@ -883,34 +889,15 @@ by blast -subsubsection {* Some proof tools *} +subsubsection {* Some rules with @{text "if"} *} text{* Elimination of @{text"{x. \ & x=t & \}"}. *} lemma Collect_conv_if: "{x. x=a & P x} = (if P a then {a} else {})" -by auto + by auto lemma Collect_conv_if2: "{x. a=x & P x} = (if P a then {a} else {})" -by auto - -text {* -Simproc for pulling @{text "x=t"} in @{text "{x. \ & x=t & \}"} -to the front (and similarly for @{text "t=x"}): -*} - -ML{* - local - val Coll_perm_tac = rtac @{thm Collect_cong} 1 THEN rtac @{thm iffI} 1 THEN - ALLGOALS(EVERY'[REPEAT_DETERM o (etac @{thm conjE}), - DEPTH_SOLVE_1 o (ares_tac [@{thm conjI}])]) - in - val defColl_regroup = Simplifier.simproc @{theory} - "defined Collect" ["{x. P x & Q x}"] - (Quantifier1.rearrange_Coll Coll_perm_tac) - end; - - Addsimprocs [defColl_regroup]; -*} + by auto text {* Rewrite rules for boolean case-splitting: faster than @{text @@ -945,13 +932,6 @@ ("Collect", [CollectD]), ("Inter", [InterD]), ("INTER", [INT_D])] *) -ML {* - val mksimps_pairs = [(@{const_name Ball}, @{thms bspec})] @ mksimps_pairs; -*} -declaration {* fn _ => - Simplifier.map_ss (fn ss => ss setmksimps (mksimps mksimps_pairs)) -*} - subsection {* Complete lattices *} @@ -1029,10 +1009,10 @@ using top_greatest [of x] by (simp add: le_iff_inf inf_commute) definition SUPR :: "'b set \ ('b \ 'a) \ 'a" where - "SUPR A f == \ (f ` A)" + "SUPR A f = \ (f ` A)" definition INFI :: "'b set \ ('b \ 'a) \ 'a" where - "INFI A f == \ (f ` A)" + "INFI A f = \ (f ` A)" end @@ -1052,17 +1032,10 @@ "INF x. B" == "INF x:CONST UNIV. B" "INF x:A. B" == "CONST INFI A (%x. B)" -(* To avoid eta-contraction of body: *) -print_translation {* -let - fun btr' syn (A :: Abs abs :: ts) = - let val (x,t) = atomic_abs_tr' abs - in list_comb (Syntax.const syn $ x $ A $ t, ts) end - val const_syntax_name = Sign.const_syntax_name @{theory} o fst o dest_Const -in -[(const_syntax_name @{term SUPR}, btr' "_SUP"),(const_syntax_name @{term "INFI"}, btr' "_INF")] -end -*} +print_translation {* [ +Syntax.preserve_binder_abs2_tr' @{const_syntax SUPR} "_SUP", +Syntax.preserve_binder_abs2_tr' @{const_syntax INFI} "_INF" +] *} -- {* to avoid eta-contraction of body *} context complete_lattice begin @@ -1112,6 +1085,24 @@ "\ \{}" unfolding Sup_bool_def by auto +lemma INFI_bool_eq: + "INFI = Ball" +proof (rule ext)+ + fix A :: "'a set" + fix P :: "'a \ bool" + show "(INF x:A. P x) \ (\x \ A. P x)" + by (auto simp add: Ball_def INFI_def Inf_bool_def) +qed + +lemma SUPR_bool_eq: + "SUPR = Bex" +proof (rule ext)+ + fix A :: "'a set" + fix P :: "'a \ bool" + show "(SUP x:A. P x) \ (\x \ A. P x)" + by (auto simp add: Bex_def SUPR_def Sup_bool_def) +qed + instantiation "fun" :: (type, complete_lattice) complete_lattice begin @@ -1136,10 +1127,43 @@ by rule (simp add: Sup_fun_def, simp add: empty_def) +subsubsection {* Union *} + +definition Union :: "'a set set \ 'a set" where + Union_eq [code del]: "Union A = {x. \B \ A. x \ B}" + +notation (xsymbols) + Union ("\_" [90] 90) + +lemma Sup_set_eq: + "\S = \S" +proof (rule set_ext) + fix x + have "(\Q\{P. \A\S. P \ x \ A}. Q) \ (\A\S. x \ A)" + by auto + then show "x \ \S \ x \ \S" + by (simp add: Sup_fun_def Sup_bool_def Union_eq) (simp add: mem_def) +qed + +lemma Union_iff [simp, noatp]: + "A \ \C \ (\X\C. A\X)" + by (unfold Union_eq) blast + +lemma UnionI [intro]: + "X \ C \ A \ X \ A \ \C" + -- {* The order of the premises presupposes that @{term C} is rigid; + @{term A} may be flexible. *} + by auto + +lemma UnionE [elim!]: + "A \ \C \ (\X. A\X \ X\C \ R) \ R" + by auto + + subsubsection {* Unions of families *} definition UNION :: "'a set \ ('a \ 'b set) \ 'b set" where - "UNION A B \ {y. \x\A. y \ B x}" + UNION_eq_Union_image: "UNION A B = \(B`A)" syntax "@UNION1" :: "pttrns => 'b set => 'b set" ("(3UN _./ _)" [0, 10] 10) @@ -1168,17 +1192,26 @@ subscripts in Proof General. *} -(* To avoid eta-contraction of body: *) -print_translation {* -let - fun btr' syn [A, Abs abs] = - let val (x, t) = atomic_abs_tr' abs - in Syntax.const syn $ x $ A $ t end -in [(@{const_syntax UNION}, btr' "@UNION")] end -*} - -declare UNION_def [noatp] - +print_translation {* [ +Syntax.preserve_binder_abs2_tr' @{const_syntax UNION} "@UNION" +] *} -- {* to avoid eta-contraction of body *} + +lemma SUPR_set_eq: + "(SUP x:S. f x) = (\x\S. f x)" + by (simp add: SUPR_def UNION_eq_Union_image Sup_set_eq) + +lemma Union_def: + "\S = (\x\S. x)" + by (simp add: UNION_eq_Union_image image_def) + +lemma UNION_def [noatp]: + "UNION A B = {y. \x\A. y \ B x}" + by (auto simp add: UNION_eq_Union_image Union_eq) + +lemma Union_image_eq [simp]: + "\(B`A) = (\x\A. B x)" + by (rule sym) (fact UNION_eq_Union_image) + lemma UN_iff [simp]: "(b: (UN x:A. B x)) = (EX x:A. b: B x)" by (unfold UNION_def) blast @@ -1202,10 +1235,49 @@ by blast +subsubsection {* Inter *} + +definition Inter :: "'a set set \ 'a set" where + Inter_eq [code del]: "Inter A = {x. \B \ A. x \ B}" + +notation (xsymbols) + Inter ("\_" [90] 90) + +lemma Inf_set_eq: + "\S = \S" +proof (rule set_ext) + fix x + have "(\Q\{P. \A\S. P \ x \ A}. Q) \ (\A\S. x \ A)" + by auto + then show "x \ \S \ x \ \S" + by (simp add: Inter_eq Inf_fun_def Inf_bool_def) (simp add: mem_def) +qed + +lemma Inter_iff [simp,noatp]: "(A : Inter C) = (ALL X:C. A:X)" + by (unfold Inter_eq) blast + +lemma InterI [intro!]: "(!!X. X:C ==> A:X) ==> A : Inter C" + by (simp add: Inter_eq) + +text {* + \medskip A ``destruct'' rule -- every @{term X} in @{term C} + contains @{term A} as an element, but @{prop "A:X"} can hold when + @{prop "X:C"} does not! This rule is analogous to @{text spec}. +*} + +lemma InterD [elim]: "A : Inter C ==> X:C ==> A:X" + by auto + +lemma InterE [elim]: "A : Inter C ==> (X~:C ==> R) ==> (A:X ==> R) ==> R" + -- {* ``Classical'' elimination rule -- does not require proving + @{prop "X:C"}. *} + by (unfold Inter_eq) blast + + subsubsection {* Intersections of families *} definition INTER :: "'a set \ ('a \ 'b set) \ 'b set" where - "INTER A B \ {y. \x\A. y \ B x}" + INTER_eq_Inter_image: "INTER A B = \(B`A)" syntax "@INTER1" :: "pttrns => 'b set => 'b set" ("(3INT _./ _)" [0, 10] 10) @@ -1225,14 +1297,25 @@ "INT x. B" == "INT x:CONST UNIV. B" "INT x:A. B" == "CONST INTER A (%x. B)" -(* To avoid eta-contraction of body: *) -print_translation {* -let - fun btr' syn [A, Abs abs] = - let val (x, t) = atomic_abs_tr' abs - in Syntax.const syn $ x $ A $ t end -in [(@{const_syntax INTER}, btr' "@INTER")] end -*} +print_translation {* [ +Syntax.preserve_binder_abs2_tr' @{const_syntax INTER} "@INTER" +] *} -- {* to avoid eta-contraction of body *} + +lemma INFI_set_eq: + "(INF x:S. f x) = (\x\S. f x)" + by (simp add: INFI_def INTER_eq_Inter_image Inf_set_eq) + +lemma Inter_def: + "Inter S = INTER S (\x. x)" + by (simp add: INTER_eq_Inter_image image_def) + +lemma INTER_def: + "INTER A B = {y. \x\A. y \ B x}" + by (auto simp add: INTER_eq_Inter_image Inter_eq) + +lemma Inter_image_eq [simp]: + "\(B`A) = (\x\A. B x)" + by (rule sym) (fact INTER_eq_Inter_image) lemma INT_iff [simp]: "(b: (INT x:A. B x)) = (ALL x:A. b: B x)" by (unfold INTER_def) blast @@ -1252,99 +1335,6 @@ by (simp add: INTER_def) -subsubsection {* Union *} - -definition Union :: "'a set set \ 'a set" where - "Union S \ UNION S (\x. x)" - -notation (xsymbols) - Union ("\_" [90] 90) - -lemma Union_image_eq [simp]: - "\(B`A) = (\x\A. B x)" - by (auto simp add: Union_def UNION_def image_def) - -lemma Union_eq: - "\A = {x. \B \ A. x \ B}" - by (simp add: Union_def UNION_def) - -lemma Sup_set_eq: - "\S = \S" -proof (rule set_ext) - fix x - have "(\Q\{P. \A\S. P \ x \ A}. Q) \ (\A\S. x \ A)" - by auto - then show "x \ \S \ x \ \S" - by (simp add: Union_eq Sup_fun_def Sup_bool_def) (simp add: mem_def) -qed - -lemma SUPR_set_eq: - "(SUP x:S. f x) = (\x\S. f x)" - by (simp add: SUPR_def Sup_set_eq) - -lemma Union_iff [simp,noatp]: "(A : Union C) = (EX X:C. A:X)" - by (unfold Union_def) blast - -lemma UnionI [intro]: "X:C ==> A:X ==> A : Union C" - -- {* The order of the premises presupposes that @{term C} is rigid; - @{term A} may be flexible. *} - by auto - -lemma UnionE [elim!]: "A : Union C ==> (!!X. A:X ==> X:C ==> R) ==> R" - by (unfold Union_def) blast - - -subsubsection {* Inter *} - -definition Inter :: "'a set set \ 'a set" where - "Inter S \ INTER S (\x. x)" - -notation (xsymbols) - Inter ("\_" [90] 90) - -lemma Inter_image_eq [simp]: - "\(B`A) = (\x\A. B x)" - by (auto simp add: Inter_def INTER_def image_def) - -lemma Inter_eq: - "\A = {x. \B \ A. x \ B}" - by (simp add: Inter_def INTER_def) - -lemma Inf_set_eq: - "\S = \S" -proof (rule set_ext) - fix x - have "(\Q\{P. \A\S. P \ x \ A}. Q) \ (\A\S. x \ A)" - by auto - then show "x \ \S \ x \ \S" - by (simp add: Inter_eq Inf_fun_def Inf_bool_def) (simp add: mem_def) -qed - -lemma INFI_set_eq: - "(INF x:S. f x) = (\x\S. f x)" - by (simp add: INFI_def Inf_set_eq) - -lemma Inter_iff [simp,noatp]: "(A : Inter C) = (ALL X:C. A:X)" - by (unfold Inter_def) blast - -lemma InterI [intro!]: "(!!X. X:C ==> A:X) ==> A : Inter C" - by (simp add: Inter_def) - -text {* - \medskip A ``destruct'' rule -- every @{term X} in @{term C} - contains @{term A} as an element, but @{prop "A:X"} can hold when - @{prop "X:C"} does not! This rule is analogous to @{text spec}. -*} - -lemma InterD [elim]: "A : Inter C ==> X:C ==> A:X" - by auto - -lemma InterE [elim]: "A : Inter C ==> (X~:C ==> R) ==> (A:X ==> R) ==> R" - -- {* ``Classical'' elimination rule -- does not require proving - @{prop "X:C"}. *} - by (unfold Inter_def) blast - - no_notation less_eq (infix "\" 50) and less (infix "\" 50) and @@ -2467,23 +2457,24 @@ text {* Rudimentary code generation *} -lemma empty_code [code]: "{} x \ False" - unfolding empty_def Collect_def .. - -lemma UNIV_code [code]: "UNIV x \ True" - unfolding UNIV_def Collect_def .. +lemma [code]: "{} = bot" + by (rule sym) (fact bot_set_eq) + +lemma [code]: "UNIV = top" + by (rule sym) (fact top_set_eq) + +lemma [code]: "op \ = inf" + by (rule ext)+ (simp add: inf_set_eq) + +lemma [code]: "op \ = sup" + by (rule ext)+ (simp add: sup_set_eq) lemma insert_code [code]: "insert y A x \ y = x \ A x" - unfolding insert_def Collect_def mem_def Un_def by auto - -lemma inter_code [code]: "(A \ B) x \ A x \ B x" - unfolding Int_def Collect_def mem_def .. - -lemma union_code [code]: "(A \ B) x \ A x \ B x" - unfolding Un_def Collect_def mem_def .. + by (auto simp add: insert_compr Collect_def mem_def) lemma vimage_code [code]: "(f -` A) x = A (f x)" - unfolding vimage_def Collect_def mem_def .. + by (simp add: vimage_def Collect_def mem_def) + text {* Misc theorem and ML bindings *} diff -r 6da9c2a49fed -r 631546213601 src/HOL/Tools/Datatype/datatype.ML --- a/src/HOL/Tools/Datatype/datatype.ML Tue Jul 21 14:08:58 2009 +0200 +++ b/src/HOL/Tools/Datatype/datatype.ML Tue Jul 21 17:02:18 2009 +0200 @@ -552,8 +552,7 @@ val _ = (case fold (curry OldTerm.add_typ_tfree_names) cargs' [] \\ tvs of [] => () | vs => error ("Extra type variables on rhs: " ^ commas vs)) - in (constrs @ [((if #flat_names config then Sign.full_name tmp_thy else - Sign.full_name_path tmp_thy tname') + in (constrs @ [(Sign.full_name_path tmp_thy tname' (Binding.map_name (Syntax.const_name mx') cname), map (dtyp_of_typ new_dts) cargs')], constr_syntax' @ [(cname, mx')], sorts'') diff -r 6da9c2a49fed -r 631546213601 src/HOL/Tools/Datatype/datatype_abs_proofs.ML --- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML Tue Jul 21 14:08:58 2009 +0200 +++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML Tue Jul 21 17:02:18 2009 +0200 @@ -93,7 +93,7 @@ val _ = message config "Constructing primrec combinators ..."; val big_name = space_implode "_" new_type_names; - val thy0 = add_path (#flat_names config) big_name thy; + val thy0 = Sign.add_path big_name thy; val descr' = List.concat descr; val recTs = get_rec_types descr' sorts; @@ -243,7 +243,7 @@ Const ("The", (T' --> HOLogic.boolT) --> T') $ absfree ("y", T', set $ Free ("x", T) $ Free ("y", T')))))) (reccomb_names ~~ reccombs ~~ rec_sets ~~ recTs ~~ rec_result_Ts)) - ||> parent_path (#flat_names config) + ||> Sign.parent_path ||> Theory.checkpoint; @@ -277,7 +277,7 @@ let val _ = message config "Proving characteristic theorems for case combinators ..."; - val thy1 = add_path (#flat_names config) (space_implode "_" new_type_names) thy; + val thy1 = Sign.add_path (space_implode "_" new_type_names) thy; val descr' = List.concat descr; val recTs = get_rec_types descr' sorts; @@ -339,7 +339,7 @@ thy2 |> Context.the_theory o fold (fold Nitpick_Const_Simps.add_thm) case_thms o Context.Theory - |> parent_path (#flat_names config) + |> Sign.parent_path |> store_thmss "cases" new_type_names case_thms |-> (fn thmss => pair (thmss, case_names)) end; diff -r 6da9c2a49fed -r 631546213601 src/HOL/Tools/Datatype/datatype_aux.ML --- a/src/HOL/Tools/Datatype/datatype_aux.ML Tue Jul 21 14:08:58 2009 +0200 +++ b/src/HOL/Tools/Datatype/datatype_aux.ML Tue Jul 21 17:02:18 2009 +0200 @@ -22,9 +22,6 @@ val message : config -> string -> unit - val add_path : bool -> string -> theory -> theory - val parent_path : bool -> theory -> theory - val store_thmss_atts : string -> string list -> attribute list list -> thm list list -> theory -> thm list list * theory val store_thmss : string -> string list -> thm list list -> theory -> thm list list * theory @@ -76,15 +73,12 @@ (* datatype option flags *) -type config = { strict: bool, flat_names: bool, quiet: bool }; +type config = { strict: bool, quiet: bool }; val default_config : config = - { strict = true, flat_names = false, quiet = false }; + { strict = true, quiet = false }; fun message ({ quiet, ...} : config) s = if quiet then () else writeln s; -fun add_path flat_names s = if flat_names then I else Sign.add_path s; -fun parent_path flat_names = if flat_names then I else Sign.parent_path; - (* store theorems in theory *) diff -r 6da9c2a49fed -r 631546213601 src/HOL/Tools/Datatype/datatype_rep_proofs.ML --- a/src/HOL/Tools/Datatype/datatype_rep_proofs.ML Tue Jul 21 14:08:58 2009 +0200 +++ b/src/HOL/Tools/Datatype/datatype_rep_proofs.ML Tue Jul 21 17:02:18 2009 +0200 @@ -66,7 +66,7 @@ val descr' = flat descr; val big_name = space_implode "_" new_type_names; - val thy1 = add_path (#flat_names config) big_name thy; + val thy1 = Sign.add_path big_name thy; val big_rec_name = big_name ^ "_rep_set"; val rep_set_names' = (if length descr' = 1 then [big_rec_name] else @@ -187,7 +187,7 @@ (********************************* typedef ********************************) val (typedefs, thy3) = thy2 |> - parent_path (#flat_names config) |> + Sign.parent_path |> fold_map (fn ((((name, mx), tvs), c), name') => Typedef.add_typedef false (SOME (Binding.name name')) (name, tvs, mx) (Collect $ Const (c, UnivT')) NONE @@ -196,7 +196,7 @@ (resolve_tac rep_intrs 1))) (types_syntax ~~ tyvars ~~ (Library.take (length newTs, rep_set_names)) ~~ new_type_names) ||> - add_path (#flat_names config) big_name; + Sign.add_path big_name; (*********************** definition of constructors ***********************) @@ -254,14 +254,14 @@ val cong' = standard (cterm_instantiate [(cterm_of thy cong_f, rep_const)] arg_cong); val dist = standard (cterm_instantiate [(cterm_of thy distinct_f, rep_const)] distinct_lemma); val (thy', defs', eqns', _) = Library.foldl ((make_constr_def tname T) (length constrs)) - ((add_path (#flat_names config) tname thy, defs, [], 1), constrs ~~ constr_syntax) + ((Sign.add_path tname thy, defs, [], 1), constrs ~~ constr_syntax) in - (parent_path (#flat_names config) thy', defs', eqns @ [eqns'], + (Sign.parent_path thy', defs', eqns @ [eqns'], rep_congs @ [cong'], dist_lemmas @ [dist]) end; val (thy4, constr_defs, constr_rep_eqns, rep_congs, dist_lemmas) = Library.foldl dt_constr_defs - ((thy3 |> Sign.add_consts_i iso_decls |> parent_path (#flat_names config), [], [], [], []), + ((thy3 |> Sign.add_consts_i iso_decls |> Sign.parent_path, [], [], [], []), hd descr ~~ new_type_names ~~ newTs ~~ constr_syntax); (*********** isomorphisms for new types (introduced by typedef) ***********) @@ -355,7 +355,7 @@ in (thy', char_thms' @ char_thms) end; val (thy5, iso_char_thms) = apfst Theory.checkpoint (List.foldr make_iso_defs - (add_path (#flat_names config) big_name thy4, []) (tl descr)); + (Sign.add_path big_name thy4, []) (tl descr)); (* prove isomorphism properties *) @@ -565,7 +565,7 @@ val ((constr_inject', distinct_thms'), thy6) = thy5 - |> parent_path (#flat_names config) + |> Sign.parent_path |> store_thmss "inject" new_type_names constr_inject ||>> store_thmss "distinct" new_type_names distinct_thms; diff -r 6da9c2a49fed -r 631546213601 src/HOL/Tools/inductive_realizer.ML --- a/src/HOL/Tools/inductive_realizer.ML Tue Jul 21 14:08:58 2009 +0200 +++ b/src/HOL/Tools/inductive_realizer.ML Tue Jul 21 17:02:18 2009 +0200 @@ -308,7 +308,7 @@ val ((dummies, some_dt_names), thy2) = thy1 |> add_dummies (Datatype.add_datatype - { strict = false, flat_names = false, quiet = false } (map (Binding.name_of o #2) dts)) + { strict = false, quiet = false } (map (Binding.name_of o #2) dts)) (map (pair false) dts) [] ||> Extraction.add_typeof_eqns_i ty_eqs ||> Extraction.add_realizes_eqns_i rlz_eqs; diff -r 6da9c2a49fed -r 631546213601 src/HOLCF/Domain.thy --- a/src/HOLCF/Domain.thy Tue Jul 21 14:08:58 2009 +0200 +++ b/src/HOLCF/Domain.thy Tue Jul 21 17:02:18 2009 +0200 @@ -9,11 +9,11 @@ uses ("Tools/cont_consts.ML") ("Tools/cont_proc.ML") - ("Tools/domain/domain_library.ML") - ("Tools/domain/domain_syntax.ML") - ("Tools/domain/domain_axioms.ML") - ("Tools/domain/domain_theorems.ML") - ("Tools/domain/domain_extender.ML") + ("Tools/Domain/domain_library.ML") + ("Tools/Domain/domain_syntax.ML") + ("Tools/Domain/domain_axioms.ML") + ("Tools/Domain/domain_theorems.ML") + ("Tools/Domain/domain_extender.ML") begin defaultsort pcpo @@ -274,10 +274,10 @@ use "Tools/cont_consts.ML" use "Tools/cont_proc.ML" -use "Tools/domain/domain_library.ML" -use "Tools/domain/domain_syntax.ML" -use "Tools/domain/domain_axioms.ML" -use "Tools/domain/domain_theorems.ML" -use "Tools/domain/domain_extender.ML" +use "Tools/Domain/domain_library.ML" +use "Tools/Domain/domain_syntax.ML" +use "Tools/Domain/domain_axioms.ML" +use "Tools/Domain/domain_theorems.ML" +use "Tools/Domain/domain_extender.ML" end diff -r 6da9c2a49fed -r 631546213601 src/HOLCF/IsaMakefile --- a/src/HOLCF/IsaMakefile Tue Jul 21 14:08:58 2009 +0200 +++ b/src/HOLCF/IsaMakefile Tue Jul 21 17:02:18 2009 +0200 @@ -62,11 +62,11 @@ Tools/adm_tac.ML \ Tools/cont_consts.ML \ Tools/cont_proc.ML \ - Tools/domain/domain_extender.ML \ - Tools/domain/domain_axioms.ML \ - Tools/domain/domain_library.ML \ - Tools/domain/domain_syntax.ML \ - Tools/domain/domain_theorems.ML \ + Tools/Domain/domain_extender.ML \ + Tools/Domain/domain_axioms.ML \ + Tools/Domain/domain_library.ML \ + Tools/Domain/domain_syntax.ML \ + Tools/Domain/domain_theorems.ML \ Tools/fixrec.ML \ Tools/pcpodef.ML \ holcf_logic.ML \ diff -r 6da9c2a49fed -r 631546213601 src/HOLCF/Tools/Domain/domain_axioms.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOLCF/Tools/Domain/domain_axioms.ML Tue Jul 21 17:02:18 2009 +0200 @@ -0,0 +1,235 @@ +(* Title: HOLCF/Tools/Domain/domain_axioms.ML + Author: David von Oheimb + +Syntax generator for domain command. +*) + +signature DOMAIN_AXIOMS = +sig + val copy_of_dtyp : (int -> term) -> Datatype.dtyp -> term + + val calc_axioms : + string -> Domain_Library.eq list -> int -> Domain_Library.eq -> + string * (string * term) list * (string * term) list + + val add_axioms : + bstring -> Domain_Library.eq list -> theory -> theory +end; + + +structure Domain_Axioms :> DOMAIN_AXIOMS = +struct + +open Domain_Library; + +infixr 0 ===>;infixr 0 ==>;infix 0 == ; +infix 1 ===; infix 1 ~= ; infix 1 <<; infix 1 ~<<; +infix 9 ` ; infix 9 `% ; infix 9 `%%; infixr 9 oo; + +(* FIXME: use theory data for this *) +val copy_tab : string Symtab.table = + Symtab.make [(@{type_name "->"}, @{const_name "cfun_fun"}), + (@{type_name "++"}, @{const_name "ssum_fun"}), + (@{type_name "**"}, @{const_name "sprod_fun"}), + (@{type_name "*"}, @{const_name "cprod_fun"}), + (@{type_name "u"}, @{const_name "u_fun"})]; + +fun copy_of_dtyp r dt = if DatatypeAux.is_rec_type dt then copy r dt else ID +and copy r (DatatypeAux.DtRec i) = r i + | copy r (DatatypeAux.DtTFree a) = ID + | copy r (DatatypeAux.DtType (c, ds)) = + case Symtab.lookup copy_tab c of + SOME f => list_ccomb (%%:f, map (copy_of_dtyp r) ds) + | NONE => (warning ("copy_of_dtyp: unknown type constructor " ^ c); ID); + +fun calc_axioms + (comp_dname : string) + (eqs : eq list) + (n : int) + (eqn as ((dname,_),cons) : eq) + : string * (string * term) list * (string * term) list = + let + + (* ----- axioms and definitions concerning the isomorphism ------------------ *) + + val dc_abs = %%:(dname^"_abs"); + val dc_rep = %%:(dname^"_rep"); + val x_name'= "x"; + val x_name = idx_name eqs x_name' (n+1); + val dnam = Long_Name.base_name dname; + + val abs_iso_ax = ("abs_iso", mk_trp(dc_rep`(dc_abs`%x_name') === %:x_name')); + val rep_iso_ax = ("rep_iso", mk_trp(dc_abs`(dc_rep`%x_name') === %:x_name')); + + val when_def = ("when_def",%%:(dname^"_when") == + List.foldr (uncurry /\ ) (/\x_name'((when_body cons (fn (x,y) => + Bound(1+length cons+x-y)))`(dc_rep`Bound 0))) (when_funs cons)); + + val copy_def = + let fun r i = cproj (Bound 0) eqs i; + in ("copy_def", %%:(dname^"_copy") == + /\ "f" (dc_abs oo (copy_of_dtyp r (dtyp_of_eq eqn)) oo dc_rep)) end; + + (* -- definitions concerning the constructors, discriminators and selectors - *) + + fun con_def m n (_,args) = let + fun idxs z x arg = (if is_lazy arg then mk_up else I) (Bound(z-x)); + fun parms vs = mk_stuple (mapn (idxs(length vs)) 1 vs); + fun inj y 1 _ = y + | inj y _ 0 = mk_sinl y + | inj y i j = mk_sinr (inj y (i-1) (j-1)); + in List.foldr /\# (dc_abs`(inj (parms args) m n)) args end; + + val con_defs = mapn (fn n => fn (con,args) => + (extern_name con ^"_def", %%:con == con_def (length cons) n (con,args))) 0 cons; + + val dis_defs = let + fun ddef (con,_) = (dis_name con ^"_def",%%:(dis_name con) == + list_ccomb(%%:(dname^"_when"),map + (fn (con',args) => (List.foldr /\# + (if con'=con then TT else FF) args)) cons)) + in map ddef cons end; + + val mat_defs = + let + fun mdef (con,_) = + let + val k = Bound 0 + val x = Bound 1 + fun one_con (con', args') = + if con'=con then k else List.foldr /\# mk_fail args' + val w = list_ccomb(%%:(dname^"_when"), map one_con cons) + val rhs = /\ "x" (/\ "k" (w ` x)) + in (mat_name con ^"_def", %%:(mat_name con) == rhs) end + in map mdef cons end; + + val pat_defs = + let + fun pdef (con,args) = + let + val ps = mapn (fn n => fn _ => %:("pat" ^ string_of_int n)) 1 args; + val xs = map (bound_arg args) args; + val r = Bound (length args); + val rhs = case args of [] => mk_return HOLogic.unit + | _ => mk_ctuple_pat ps ` mk_ctuple xs; + fun one_con (con',args') = List.foldr /\# (if con'=con then rhs else mk_fail) args'; + in (pat_name con ^"_def", list_comb (%%:(pat_name con), ps) == + list_ccomb(%%:(dname^"_when"), map one_con cons)) + end + in map pdef cons end; + + val sel_defs = let + fun sdef con n arg = Option.map (fn sel => (sel^"_def",%%:sel == + list_ccomb(%%:(dname^"_when"),map + (fn (con',args) => if con'<>con then UU else + List.foldr /\# (Bound (length args - n)) args) cons))) (sel_of arg); + in List.mapPartial I (List.concat(map (fn (con,args) => mapn (sdef con) 1 args) cons)) end; + + + (* ----- axiom and definitions concerning induction ------------------------- *) + + val reach_ax = ("reach", mk_trp(cproj (mk_fix (%%:(comp_dname^"_copy"))) eqs n + `%x_name === %:x_name)); + val take_def = + ("take_def", + %%:(dname^"_take") == + mk_lam("n",cproj + (mk_iterate (Bound 0, %%:(comp_dname^"_copy"), UU)) eqs n)); + val finite_def = + ("finite_def", + %%:(dname^"_finite") == + mk_lam(x_name, + mk_ex("n",(%%:(dname^"_take") $ Bound 0)`Bound 1 === Bound 1))); + + in (dnam, + [abs_iso_ax, rep_iso_ax, reach_ax], + [when_def, copy_def] @ + con_defs @ dis_defs @ mat_defs @ pat_defs @ sel_defs @ + [take_def, finite_def]) + end; (* let (calc_axioms) *) + + +(* legacy type inference *) + +fun legacy_infer_term thy t = + singleton (Syntax.check_terms (ProofContext.init thy)) (Sign.intern_term thy t); + +fun legacy_infer_prop thy t = legacy_infer_term thy (TypeInfer.constrain propT t); + +fun infer_props thy = map (apsnd (legacy_infer_prop thy)); + + +fun add_axioms_i x = snd o PureThy.add_axioms (map (Thm.no_attributes o apfst Binding.name) x); +fun add_axioms_infer axms thy = add_axioms_i (infer_props thy axms) thy; + +fun add_defs_i x = snd o (PureThy.add_defs false) (map (Thm.no_attributes o apfst Binding.name) x); +fun add_defs_infer defs thy = add_defs_i (infer_props thy defs) thy; + +fun add_matchers (((dname,_),cons) : eq) thy = + let + val con_names = map fst cons; + val mat_names = map mat_name con_names; + fun qualify n = Sign.full_name thy (Binding.name n); + val ms = map qualify con_names ~~ map qualify mat_names; + in Fixrec.add_matchers ms thy end; + +fun add_axioms comp_dnam (eqs : eq list) thy' = + let + val comp_dname = Sign.full_bname thy' comp_dnam; + val dnames = map (fst o fst) eqs; + val x_name = idx_name dnames "x"; + fun copy_app dname = %%:(dname^"_copy")`Bound 0; + val copy_def = ("copy_def" , %%:(comp_dname^"_copy") == + /\ "f"(mk_ctuple (map copy_app dnames))); + + fun one_con (con,args) = let + val nonrec_args = filter_out is_rec args; + val rec_args = List.filter is_rec args; + val recs_cnt = length rec_args; + val allargs = nonrec_args @ rec_args + @ map (upd_vname (fn s=> s^"'")) rec_args; + val allvns = map vname allargs; + fun vname_arg s arg = if is_rec arg then vname arg^s else vname arg; + val vns1 = map (vname_arg "" ) args; + val vns2 = map (vname_arg "'") args; + val allargs_cnt = length nonrec_args + 2*recs_cnt; + val rec_idxs = (recs_cnt-1) downto 0; + val nonlazy_idxs = map snd (filter_out (fn (arg,_) => is_lazy arg) + (allargs~~((allargs_cnt-1) downto 0))); + fun rel_app i ra = proj (Bound(allargs_cnt+2)) eqs (rec_of ra) $ + Bound (2*recs_cnt-i) $ Bound (recs_cnt-i); + val capps = + List.foldr mk_conj + (mk_conj( + Bound(allargs_cnt+1)===list_ccomb(%%:con,map (bound_arg allvns) vns1), + Bound(allargs_cnt+0)===list_ccomb(%%:con,map (bound_arg allvns) vns2))) + (mapn rel_app 1 rec_args); + in List.foldr mk_ex + (Library.foldr mk_conj + (map (defined o Bound) nonlazy_idxs,capps)) allvns + end; + fun one_comp n (_,cons) = + mk_all(x_name(n+1), + mk_all(x_name(n+1)^"'", + mk_imp(proj (Bound 2) eqs n $ Bound 1 $ Bound 0, + foldr1 mk_disj (mk_conj(Bound 1 === UU,Bound 0 === UU) + ::map one_con cons)))); + val bisim_def = + ("bisim_def", + %%:(comp_dname^"_bisim")==mk_lam("R", foldr1 mk_conj (mapn one_comp 0 eqs))); + + fun add_one (thy,(dnam,axs,dfs)) = + thy |> Sign.add_path dnam + |> add_defs_infer dfs + |> add_axioms_infer axs + |> Sign.parent_path; + + val thy = Library.foldl add_one (thy', mapn (calc_axioms comp_dname eqs) 0 eqs); + + in thy |> Sign.add_path comp_dnam + |> add_defs_infer (bisim_def::(if length eqs>1 then [copy_def] else [])) + |> Sign.parent_path + |> fold add_matchers eqs + end; (* let (add_axioms) *) + +end; (* struct *) diff -r 6da9c2a49fed -r 631546213601 src/HOLCF/Tools/Domain/domain_extender.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOLCF/Tools/Domain/domain_extender.ML Tue Jul 21 17:02:18 2009 +0200 @@ -0,0 +1,204 @@ +(* Title: HOLCF/Tools/Domain/domain_extender.ML + Author: David von Oheimb + +Theory extender for domain command, including theory syntax. +*) + +signature DOMAIN_EXTENDER = +sig + val add_domain_cmd: string -> + ((string * string option) list * binding * mixfix * + (binding * (bool * binding option * string) list * mixfix) list) list + -> theory -> theory + val add_domain: string -> + ((string * string option) list * binding * mixfix * + (binding * (bool * binding option * typ) list * mixfix) list) list + -> theory -> theory +end; + +structure Domain_Extender :> DOMAIN_EXTENDER = +struct + +open Domain_Library; + +(* ----- general testing and preprocessing of constructor list -------------- *) +fun check_and_sort_domain + (dtnvs : (string * typ list) list) + (cons'' : (binding * (bool * binding option * typ) list * mixfix) list list) + (sg : theory) + : ((string * typ list) * + (binding * (bool * binding option * typ) list * mixfix) list) list = + let + val defaultS = Sign.defaultS sg; + val test_dupl_typs = (case duplicates (op =) (map fst dtnvs) of + [] => false | dups => error ("Duplicate types: " ^ commas_quote dups)); + val test_dupl_cons = + (case duplicates (op =) (map (Binding.name_of o first) (List.concat cons'')) of + [] => false | dups => error ("Duplicate constructors: " + ^ commas_quote dups)); + val test_dupl_sels = + (case duplicates (op =) (map Binding.name_of (List.mapPartial second + (List.concat (map second (List.concat cons''))))) of + [] => false | dups => error("Duplicate selectors: "^commas_quote dups)); + val test_dupl_tvars = + exists(fn s=>case duplicates (op =) (map(fst o dest_TFree)s)of + [] => false | dups => error("Duplicate type arguments: " + ^commas_quote dups)) (map snd dtnvs); + (* test for free type variables, illegal sort constraints on rhs, + non-pcpo-types and invalid use of recursive type; + replace sorts in type variables on rhs *) + fun analyse_equation ((dname,typevars),cons') = + let + val tvars = map dest_TFree typevars; + val distinct_typevars = map TFree tvars; + fun rm_sorts (TFree(s,_)) = TFree(s,[]) + | rm_sorts (Type(s,ts)) = Type(s,remove_sorts ts) + | rm_sorts (TVar(s,_)) = TVar(s,[]) + and remove_sorts l = map rm_sorts l; + val indirect_ok = ["*","Cfun.->","Ssum.++","Sprod.**","Up.u"] + fun analyse indirect (TFree(v,s)) = + (case AList.lookup (op =) tvars v of + NONE => error ("Free type variable " ^ quote v ^ " on rhs.") + | SOME sort => if eq_set_string (s,defaultS) orelse + eq_set_string (s,sort ) + then TFree(v,sort) + else error ("Inconsistent sort constraint" ^ + " for type variable " ^ quote v)) + | analyse indirect (t as Type(s,typl)) = + (case AList.lookup (op =) dtnvs s of + NONE => if s mem indirect_ok + then Type(s,map (analyse false) typl) + else Type(s,map (analyse true) typl) + | SOME typevars => if indirect + then error ("Indirect recursion of type " ^ + quote (string_of_typ sg t)) + else if dname <> s orelse + (** BUG OR FEATURE?: + mutual recursion may use different arguments **) + remove_sorts typevars = remove_sorts typl + then Type(s,map (analyse true) typl) + else error ("Direct recursion of type " ^ + quote (string_of_typ sg t) ^ + " with different arguments")) + | analyse indirect (TVar _) = Imposs "extender:analyse"; + fun check_pcpo lazy T = + let val ok = if lazy then cpo_type else pcpo_type + in if ok sg T then T else error + ("Constructor argument type is not of sort pcpo: " ^ + string_of_typ sg T) + end; + fun analyse_arg (lazy, sel, T) = + (lazy, sel, check_pcpo lazy (analyse false T)); + fun analyse_con (b, args, mx) = (b, map analyse_arg args, mx); + in ((dname,distinct_typevars), map analyse_con cons') end; + in ListPair.map analyse_equation (dtnvs,cons'') + end; (* let *) + +(* ----- calls for building new thy and thms -------------------------------- *) + +fun gen_add_domain + (prep_typ : theory -> 'a -> typ) + (comp_dnam : string) + (eqs''' : ((string * string option) list * binding * mixfix * + (binding * (bool * binding option * 'a) list * mixfix) list) list) + (thy''' : theory) = + let + fun readS (SOME s) = Syntax.read_sort_global thy''' s + | readS NONE = Sign.defaultS thy'''; + fun readTFree (a, s) = TFree (a, readS s); + + val dtnvs = map (fn (vs,dname:binding,mx,_) => + (dname, map readTFree vs, mx)) eqs'''; + val cons''' = map (fn (_,_,_,cons) => cons) eqs'''; + fun thy_type (dname,tvars,mx) = (dname, length tvars, mx); + fun thy_arity (dname,tvars,mx) = (Sign.full_name thy''' dname, map (snd o dest_TFree) tvars, pcpoS); + val thy'' = thy''' |> Sign.add_types (map thy_type dtnvs) + |> fold (AxClass.axiomatize_arity o thy_arity) dtnvs; + val cons'' = map (map (upd_second (map (upd_third (prep_typ thy''))))) cons'''; + val dtnvs' = map (fn (dname,vs,mx) => (Sign.full_name thy''' dname,vs)) dtnvs; + val eqs' : ((string * typ list) * (binding * (bool * binding option * typ) list * mixfix) list) list = + check_and_sort_domain dtnvs' cons'' thy''; + val thy' = thy'' |> Domain_Syntax.add_syntax comp_dnam eqs'; + val dts = map (Type o fst) eqs'; + val new_dts = map (fn ((s,Ts),_) => (s, map (fst o dest_TFree) Ts)) eqs'; + fun strip ss = Library.drop (find_index (fn s => s = "'") ss + 1, ss); + fun typid (Type (id,_)) = + let val c = hd (Symbol.explode (Long_Name.base_name id)) + in if Symbol.is_letter c then c else "t" end + | typid (TFree (id,_) ) = hd (strip (tl (Symbol.explode id))) + | typid (TVar ((id,_),_)) = hd (tl (Symbol.explode id)); + fun one_con (con,args,mx) = + ((Syntax.const_name mx (Binding.name_of con)), + ListPair.map (fn ((lazy,sel,tp),vn) => mk_arg ((lazy, + DatatypeAux.dtyp_of_typ new_dts tp), + Option.map Binding.name_of sel,vn)) + (args,(mk_var_names(map (typid o third) args))) + ) : cons; + val eqs = map (fn (dtnvs,cons') => (dtnvs, map one_con cons')) eqs' : eq list; + val thy = thy' |> Domain_Axioms.add_axioms comp_dnam eqs; + val ((rewss, take_rews), theorems_thy) = + thy |> fold_map (fn eq => Domain_Theorems.theorems (eq, eqs)) eqs + ||>> Domain_Theorems.comp_theorems (comp_dnam, eqs); + in + theorems_thy + |> Sign.add_path (Long_Name.base_name comp_dnam) + |> (snd o (PureThy.add_thmss [((Binding.name "rews", List.concat rewss @ take_rews), [])])) + |> Sign.parent_path + end; + +val add_domain = gen_add_domain Sign.certify_typ; +val add_domain_cmd = gen_add_domain Syntax.read_typ_global; + + +(** outer syntax **) + +local structure P = OuterParse and K = OuterKeyword in + +val _ = OuterKeyword.keyword "lazy"; + +val dest_decl : (bool * binding option * string) parser = + P.$$$ "(" |-- Scan.optional (P.$$$ "lazy" >> K true) false -- + (P.binding >> SOME) -- (P.$$$ "::" |-- P.typ) --| P.$$$ ")" >> P.triple1 + || P.$$$ "(" |-- P.$$$ "lazy" |-- P.typ --| P.$$$ ")" + >> (fn t => (true,NONE,t)) + || P.typ >> (fn t => (false,NONE,t)); + +val cons_decl = + P.binding -- Scan.repeat dest_decl -- P.opt_mixfix; + +val type_var' : (string * string option) parser = + (P.type_ident -- Scan.option (P.$$$ "::" |-- P.!!! P.sort)); + +val type_args' : (string * string option) list parser = + type_var' >> single || + P.$$$ "(" |-- P.!!! (P.list1 type_var' --| P.$$$ ")") || + Scan.succeed []; + +val domain_decl = + (type_args' -- P.binding -- P.opt_infix) -- + (P.$$$ "=" |-- P.enum1 "|" cons_decl); + +val domains_decl = + Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") -- + P.and_list1 domain_decl; + +fun mk_domain (opt_name : string option, + doms : ((((string * string option) list * binding) * mixfix) * + ((binding * (bool * binding option * string) list) * mixfix) list) list ) = + let + val names = map (fn (((_, t), _), _) => Binding.name_of t) doms; + val specs : ((string * string option) list * binding * mixfix * + (binding * (bool * binding option * string) list * mixfix) list) list = + map (fn (((vs, t), mx), cons) => + (vs, t, mx, map (fn ((c, ds), mx) => (c, ds, mx)) cons)) doms; + val comp_dnam = + case opt_name of NONE => space_implode "_" names | SOME s => s; + in add_domain_cmd comp_dnam specs end; + +val _ = + OuterSyntax.command "domain" "define recursive domains (HOLCF)" K.thy_decl + (domains_decl >> (Toplevel.theory o mk_domain)); + +end; + +end; diff -r 6da9c2a49fed -r 631546213601 src/HOLCF/Tools/Domain/domain_library.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOLCF/Tools/Domain/domain_library.ML Tue Jul 21 17:02:18 2009 +0200 @@ -0,0 +1,399 @@ +(* Title: HOLCF/Tools/Domain/domain_library.ML + Author: David von Oheimb + +Library for domain command. +*) + + +(* ----- general support ---------------------------------------------------- *) + +fun mapn f n [] = [] + | mapn f n (x::xs) = (f n x) :: mapn f (n+1) xs; + +fun foldr'' f (l,f2) = + let fun itr [] = raise Fail "foldr''" + | itr [a] = f2 a + | itr (a::l) = f(a, itr l) + in itr l end; + +fun map_cumulr f start xs = + List.foldr (fn (x,(ys,res))=>case f(x,res) of (y,res2) => + (y::ys,res2)) ([],start) xs; + +fun first (x,_,_) = x; fun second (_,x,_) = x; fun third (_,_,x) = x; +fun upd_first f (x,y,z) = (f x, y, z); +fun upd_second f (x,y,z) = ( x, f y, z); +fun upd_third f (x,y,z) = ( x, y, f z); + +fun atomize ctxt thm = + let + val r_inst = read_instantiate ctxt; + fun at thm = + case concl_of thm of + _$(Const("op &",_)$_$_) => at(thm RS conjunct1)@at(thm RS conjunct2) + | _$(Const("All" ,_)$Abs(s,_,_))=> at(thm RS (r_inst [(("x", 0), "?" ^ s)] spec)) + | _ => [thm]; + in map zero_var_indexes (at thm) end; + +(* infix syntax *) + +infixr 5 -->; +infixr 6 ->>; +infixr 0 ===>; +infixr 0 ==>; +infix 0 ==; +infix 1 ===; +infix 1 ~=; +infix 1 <<; +infix 1 ~<<; + +infix 9 ` ; +infix 9 `% ; +infix 9 `%%; + + +(* ----- specific support for domain ---------------------------------------- *) + +signature DOMAIN_LIBRARY = +sig + val Imposs : string -> 'a; + val cpo_type : theory -> typ -> bool; + val pcpo_type : theory -> typ -> bool; + val string_of_typ : theory -> typ -> string; + + (* Creating HOLCF types *) + val mk_cfunT : typ * typ -> typ; + val ->> : typ * typ -> typ; + val mk_ssumT : typ * typ -> typ; + val mk_sprodT : typ * typ -> typ; + val mk_uT : typ -> typ; + val oneT : typ; + val trT : typ; + val mk_maybeT : typ -> typ; + val mk_ctupleT : typ list -> typ; + val mk_TFree : string -> typ; + val pcpoS : sort; + + (* Creating HOLCF terms *) + val %: : string -> term; + val %%: : string -> term; + val ` : term * term -> term; + val `% : term * string -> term; + val /\ : string -> term -> term; + val UU : term; + val TT : term; + val FF : term; + val ID : term; + val oo : term * term -> term; + val mk_up : term -> term; + val mk_sinl : term -> term; + val mk_sinr : term -> term; + val mk_stuple : term list -> term; + val mk_ctuple : term list -> term; + val mk_fix : term -> term; + val mk_iterate : term * term * term -> term; + val mk_fail : term; + val mk_return : term -> term; + val cproj : term -> 'a list -> int -> term; + val list_ccomb : term * term list -> term; + (* + val con_app : string -> ('a * 'b * string) list -> term; + *) + val con_app2 : string -> ('a -> term) -> 'a list -> term; + val proj : term -> 'a list -> int -> term; + val prj : ('a -> 'b -> 'a) -> ('a -> 'b -> 'a) -> 'a -> 'b list -> int -> 'a; + val mk_ctuple_pat : term list -> term; + val mk_branch : term -> term; + + (* Creating propositions *) + val mk_conj : term * term -> term; + val mk_disj : term * term -> term; + val mk_imp : term * term -> term; + val mk_lam : string * term -> term; + val mk_all : string * term -> term; + val mk_ex : string * term -> term; + val mk_constrain : typ * term -> term; + val mk_constrainall : string * typ * term -> term; + val === : term * term -> term; + val << : term * term -> term; + val ~<< : term * term -> term; + val strict : term -> term; + val defined : term -> term; + val mk_adm : term -> term; + val mk_compact : term -> term; + val lift : ('a -> term) -> 'a list * term -> term; + val lift_defined : ('a -> term) -> 'a list * term -> term; + + (* Creating meta-propositions *) + val mk_trp : term -> term; (* HOLogic.mk_Trueprop *) + val == : term * term -> term; + val ===> : term * term -> term; + val ==> : term * term -> term; + val mk_All : string * term -> term; + + (* Domain specifications *) + eqtype arg; + type cons = string * arg list; + type eq = (string * typ list) * cons list; + val mk_arg : (bool * Datatype.dtyp) * string option * string -> arg; + val is_lazy : arg -> bool; + val rec_of : arg -> int; + val dtyp_of : arg -> Datatype.dtyp; + val sel_of : arg -> string option; + val vname : arg -> string; + val upd_vname : (string -> string) -> arg -> arg; + val is_rec : arg -> bool; + val is_nonlazy_rec : arg -> bool; + val nonlazy : arg list -> string list; + val nonlazy_rec : arg list -> string list; + val %# : arg -> term; + val /\# : arg * term -> term; + val when_body : cons list -> (int * int -> term) -> term; + val when_funs : 'a list -> string list; + val bound_arg : ''a list -> ''a -> term; (* ''a = arg or string *) + val idx_name : 'a list -> string -> int -> string; + val app_rec_arg : (int -> term) -> arg -> term; + val con_app : string -> arg list -> term; + val dtyp_of_eq : eq -> Datatype.dtyp; + + + (* Name mangling *) + val strip_esc : string -> string; + val extern_name : string -> string; + val dis_name : string -> string; + val mat_name : string -> string; + val pat_name : string -> string; + val mk_var_names : string list -> string list; +end; + +structure Domain_Library :> DOMAIN_LIBRARY = +struct + +exception Impossible of string; +fun Imposs msg = raise Impossible ("Domain:"^msg); + +(* ----- name handling ----- *) + +val strip_esc = + let fun strip ("'" :: c :: cs) = c :: strip cs + | strip ["'"] = [] + | strip (c :: cs) = c :: strip cs + | strip [] = []; + in implode o strip o Symbol.explode end; + +fun extern_name con = + case Symbol.explode con of + ("o"::"p"::" "::rest) => implode rest + | _ => con; +fun dis_name con = "is_"^ (extern_name con); +fun dis_name_ con = "is_"^ (strip_esc con); +fun mat_name con = "match_"^ (extern_name con); +fun mat_name_ con = "match_"^ (strip_esc con); +fun pat_name con = (extern_name con) ^ "_pat"; +fun pat_name_ con = (strip_esc con) ^ "_pat"; + +(* make distinct names out of the type list, + forbidding "o","n..","x..","f..","P.." as names *) +(* a number string is added if necessary *) +fun mk_var_names ids : string list = + let + fun nonreserved s = if s mem ["n","x","f","P"] then s^"'" else s; + fun index_vnames(vn::vns,occupied) = + (case AList.lookup (op =) occupied vn of + NONE => if vn mem vns + then (vn^"1") :: index_vnames(vns,(vn,1) ::occupied) + else vn :: index_vnames(vns, occupied) + | SOME(i) => (vn^(string_of_int (i+1))) + :: index_vnames(vns,(vn,i+1)::occupied)) + | index_vnames([],occupied) = []; + in index_vnames(map nonreserved ids, [("O",0),("o",0)]) end; + +fun cpo_type sg t = Sign.of_sort sg (Sign.certify_typ sg t, @{sort cpo}); +fun pcpo_type sg t = Sign.of_sort sg (Sign.certify_typ sg t, @{sort pcpo}); +fun string_of_typ sg = Syntax.string_of_typ_global sg o Sign.certify_typ sg; + +(* ----- constructor list handling ----- *) + +type arg = + (bool * Datatype.dtyp) * (* (lazy, recursive element) *) + string option * (* selector name *) + string; (* argument name *) + +type cons = + string * (* operator name of constr *) + arg list; (* argument list *) + +type eq = + (string * (* name of abstracted type *) + typ list) * (* arguments of abstracted type *) + cons list; (* represented type, as a constructor list *) + +val mk_arg = I; + +fun rec_of ((_,dtyp),_,_) = + case dtyp of DatatypeAux.DtRec i => i | _ => ~1; +(* FIXME: what about indirect recursion? *) + +fun is_lazy arg = fst (first arg); +fun dtyp_of arg = snd (first arg); +val sel_of = second; +val vname = third; +val upd_vname = upd_third; +fun is_rec arg = rec_of arg >=0; +fun is_nonlazy_rec arg = is_rec arg andalso not (is_lazy arg); +fun nonlazy args = map vname (filter_out is_lazy args); +fun nonlazy_rec args = map vname (List.filter is_nonlazy_rec args); + + +(* ----- combinators for making dtyps ----- *) + +fun mk_uD T = DatatypeAux.DtType(@{type_name "u"}, [T]); +fun mk_sprodD (T, U) = DatatypeAux.DtType(@{type_name "**"}, [T, U]); +fun mk_ssumD (T, U) = DatatypeAux.DtType(@{type_name "++"}, [T, U]); +fun mk_liftD T = DatatypeAux.DtType(@{type_name "lift"}, [T]); +val unitD = DatatypeAux.DtType(@{type_name "unit"}, []); +val boolD = DatatypeAux.DtType(@{type_name "bool"}, []); +val oneD = mk_liftD unitD; +val trD = mk_liftD boolD; +fun big_sprodD ds = case ds of [] => oneD | _ => foldr1 mk_sprodD ds; +fun big_ssumD ds = case ds of [] => unitD | _ => foldr1 mk_ssumD ds; + +fun dtyp_of_arg ((lazy, D), _, _) = if lazy then mk_uD D else D; +fun dtyp_of_cons (_, args) = big_sprodD (map dtyp_of_arg args); +fun dtyp_of_eq (_, cons) = big_ssumD (map dtyp_of_cons cons); + + +(* ----- support for type and mixfix expressions ----- *) + +fun mk_uT T = Type(@{type_name "u"}, [T]); +fun mk_cfunT (T, U) = Type(@{type_name "->"}, [T, U]); +fun mk_sprodT (T, U) = Type(@{type_name "**"}, [T, U]); +fun mk_ssumT (T, U) = Type(@{type_name "++"}, [T, U]); +val oneT = @{typ one}; +val trT = @{typ tr}; + +val op ->> = mk_cfunT; + +fun mk_TFree s = TFree ("'" ^ s, @{sort pcpo}); + +(* ----- support for term expressions ----- *) + +fun %: s = Free(s,dummyT); +fun %# arg = %:(vname arg); +fun %%: s = Const(s,dummyT); + +local open HOLogic in +val mk_trp = mk_Trueprop; +fun mk_conj (S,T) = conj $ S $ T; +fun mk_disj (S,T) = disj $ S $ T; +fun mk_imp (S,T) = imp $ S $ T; +fun mk_lam (x,T) = Abs(x,dummyT,T); +fun mk_all (x,P) = HOLogic.mk_all (x,dummyT,P); +fun mk_ex (x,P) = mk_exists (x,dummyT,P); +val mk_constrain = uncurry TypeInfer.constrain; +fun mk_constrainall (x,typ,P) = %%:"All" $ (TypeInfer.constrain (typ --> boolT) (mk_lam(x,P))); +end + +fun mk_All (x,P) = %%:"all" $ mk_lam(x,P); (* meta universal quantification *) + +infixr 0 ===>; fun S ===> T = %%:"==>" $ S $ T; +infixr 0 ==>; fun S ==> T = mk_trp S ===> mk_trp T; +infix 0 ==; fun S == T = %%:"==" $ S $ T; +infix 1 ===; fun S === T = %%:"op =" $ S $ T; +infix 1 ~=; fun S ~= T = HOLogic.mk_not (S === T); +infix 1 <<; fun S << T = %%: @{const_name Porder.below} $ S $ T; +infix 1 ~<<; fun S ~<< T = HOLogic.mk_not (S << T); + +infix 9 ` ; fun f ` x = %%: @{const_name Rep_CFun} $ f $ x; +infix 9 `% ; fun f`% s = f` %: s; +infix 9 `%%; fun f`%%s = f` %%:s; + +fun mk_adm t = %%: @{const_name adm} $ t; +fun mk_compact t = %%: @{const_name compact} $ t; +val ID = %%: @{const_name ID}; +fun mk_strictify t = %%: @{const_name strictify}`t; +fun mk_cfst t = %%: @{const_name cfst}`t; +fun mk_csnd t = %%: @{const_name csnd}`t; +(*val csplitN = "Cprod.csplit";*) +(*val sfstN = "Sprod.sfst";*) +(*val ssndN = "Sprod.ssnd";*) +fun mk_ssplit t = %%: @{const_name ssplit}`t; +fun mk_sinl t = %%: @{const_name sinl}`t; +fun mk_sinr t = %%: @{const_name sinr}`t; +fun mk_sscase (x, y) = %%: @{const_name sscase}`x`y; +fun mk_up t = %%: @{const_name up}`t; +fun mk_fup (t,u) = %%: @{const_name fup} ` t ` u; +val ONE = @{term ONE}; +val TT = @{term TT}; +val FF = @{term FF}; +fun mk_iterate (n,f,z) = %%: @{const_name iterate} $ n ` f ` z; +fun mk_fix t = %%: @{const_name fix}`t; +fun mk_return t = %%: @{const_name Fixrec.return}`t; +val mk_fail = %%: @{const_name Fixrec.fail}; + +fun mk_branch t = %%: @{const_name Fixrec.branch} $ t; + +val pcpoS = @{sort pcpo}; + +val list_ccomb = Library.foldl (op `); (* continuous version of list_comb *) +fun con_app2 con f args = list_ccomb(%%:con,map f args); +fun con_app con = con_app2 con %#; +fun if_rec arg f y = if is_rec arg then f (rec_of arg) else y; +fun app_rec_arg p arg = if_rec arg (fn n => fn x => (p n)`x) I (%# arg); +fun prj _ _ x ( _::[]) _ = x + | prj f1 _ x (_::y::ys) 0 = f1 x y + | prj f1 f2 x (y:: ys) j = prj f1 f2 (f2 x y) ys (j-1); +fun proj x = prj (fn S => K(%%:"fst" $S)) (fn S => K(%%:"snd" $S)) x; +fun cproj x = prj (fn S => K(mk_cfst S)) (fn S => K(mk_csnd S)) x; +fun lift tfn = Library.foldr (fn (x,t)=> (mk_trp(tfn x) ===> t)); + +fun /\ v T = %%: @{const_name Abs_CFun} $ mk_lam(v,T); +fun /\# (arg,T) = /\ (vname arg) T; +infixr 9 oo; fun S oo T = %%: @{const_name cfcomp}`S`T; +val UU = %%: @{const_name UU}; +fun strict f = f`UU === UU; +fun defined t = t ~= UU; +fun cpair (t,u) = %%: @{const_name cpair}`t`u; +fun spair (t,u) = %%: @{const_name spair}`t`u; +fun mk_ctuple [] = HOLogic.unit (* used in match_defs *) + | mk_ctuple ts = foldr1 cpair ts; +fun mk_stuple [] = ONE + | mk_stuple ts = foldr1 spair ts; +fun mk_ctupleT [] = HOLogic.unitT (* used in match_defs *) + | mk_ctupleT Ts = foldr1 HOLogic.mk_prodT Ts; +fun mk_maybeT T = Type ("Fixrec.maybe",[T]); +fun cpair_pat (p1,p2) = %%: @{const_name cpair_pat} $ p1 $ p2; +val mk_ctuple_pat = foldr1 cpair_pat; +fun lift_defined f = lift (fn x => defined (f x)); +fun bound_arg vns v = Bound (length vns - find_index (fn v' => v' = v) vns - 1); + +fun cont_eta_contract (Const("Cfun.Abs_CFun",TT) $ Abs(a,T,body)) = + (case cont_eta_contract body of + body' as (Const("Cfun.Rep_CFun",Ta) $ f $ Bound 0) => + if not (0 mem loose_bnos f) then incr_boundvars ~1 f + else Const("Cfun.Abs_CFun",TT) $ Abs(a,T,body') + | body' => Const("Cfun.Abs_CFun",TT) $ Abs(a,T,body')) + | cont_eta_contract(f$t) = cont_eta_contract f $ cont_eta_contract t + | cont_eta_contract t = t; + +fun idx_name dnames s n = s^(if length dnames = 1 then "" else string_of_int n); +fun when_funs cons = if length cons = 1 then ["f"] + else mapn (fn n => K("f"^(string_of_int n))) 1 cons; +fun when_body cons funarg = + let + fun one_fun n (_,[] ) = /\ "dummy" (funarg(1,n)) + | one_fun n (_,args) = let + val l2 = length args; + fun idxs m arg = (if is_lazy arg then (fn t => mk_fup (ID, t)) + else I) (Bound(l2-m)); + in cont_eta_contract + (foldr'' + (fn (a,t) => mk_ssplit (/\# (a,t))) + (args, + fn a=> /\#(a,(list_ccomb(funarg(l2,n),mapn idxs 1 args)))) + ) end; + in (if length cons = 1 andalso length(snd(hd cons)) <= 1 + then mk_strictify else I) + (foldr1 mk_sscase (mapn one_fun 1 cons)) end; + +end; (* struct *) diff -r 6da9c2a49fed -r 631546213601 src/HOLCF/Tools/Domain/domain_syntax.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOLCF/Tools/Domain/domain_syntax.ML Tue Jul 21 17:02:18 2009 +0200 @@ -0,0 +1,181 @@ +(* Title: HOLCF/Tools/Domain/domain_syntax.ML + Author: David von Oheimb + +Syntax generator for domain command. +*) + +signature DOMAIN_SYNTAX = +sig + val calc_syntax: + typ -> + (string * typ list) * + (binding * (bool * binding option * typ) list * mixfix) list -> + (binding * typ * mixfix) list * ast Syntax.trrule list + + val add_syntax: + string -> + ((string * typ list) * + (binding * (bool * binding option * typ) list * mixfix) list) list -> + theory -> theory +end; + + +structure Domain_Syntax :> DOMAIN_SYNTAX = +struct + +open Domain_Library; +infixr 5 -->; infixr 6 ->>; + +fun calc_syntax + (dtypeprod : typ) + ((dname : string, typevars : typ list), + (cons': (binding * (bool * binding option * typ) list * mixfix) list)) + : (binding * typ * mixfix) list * ast Syntax.trrule list = + let + (* ----- constants concerning the isomorphism ------------------------------- *) + + local + fun opt_lazy (lazy,_,t) = if lazy then mk_uT t else t + fun prod (_,args,_) = case args of [] => oneT + | _ => foldr1 mk_sprodT (map opt_lazy args); + fun freetvar s = let val tvar = mk_TFree s in + if tvar mem typevars then freetvar ("t"^s) else tvar end; + fun when_type (_,args,_) = List.foldr (op ->>) (freetvar "t") (map third args); + in + val dtype = Type(dname,typevars); + val dtype2 = foldr1 mk_ssumT (map prod cons'); + val dnam = Long_Name.base_name dname; + fun dbind s = Binding.name (dnam ^ s); + val const_rep = (dbind "_rep" , dtype ->> dtype2, NoSyn); + val const_abs = (dbind "_abs" , dtype2 ->> dtype , NoSyn); + val const_when = (dbind "_when", List.foldr (op ->>) (dtype ->> freetvar "t") (map when_type cons'), NoSyn); + val const_copy = (dbind "_copy", dtypeprod ->> dtype ->> dtype , NoSyn); + end; + + (* ----- constants concerning constructors, discriminators, and selectors --- *) + + local + val escape = let + fun esc (c::cs) = if c mem ["'","_","(",")","/"] then "'"::c::esc cs + else c::esc cs + | esc [] = [] + in implode o esc o Symbol.explode end; + fun dis_name_ con = Binding.name ("is_" ^ strip_esc (Binding.name_of con)); + fun mat_name_ con = Binding.name ("match_" ^ strip_esc (Binding.name_of con)); + fun pat_name_ con = Binding.name (strip_esc (Binding.name_of con) ^ "_pat"); + fun con (name,args,mx) = (name, List.foldr (op ->>) dtype (map third args), mx); + fun dis (con,args,mx) = (dis_name_ con, dtype->>trT, + Mixfix(escape ("is_" ^ Binding.name_of con), [], Syntax.max_pri)); + (* strictly speaking, these constants have one argument, + but the mixfix (without arguments) is introduced only + to generate parse rules for non-alphanumeric names*) + fun freetvar s n = let val tvar = mk_TFree (s ^ string_of_int n) in + if tvar mem typevars then freetvar ("t"^s) n else tvar end; + fun mk_matT (a,bs,c) = a ->> foldr (op ->>) (mk_maybeT c) bs ->> mk_maybeT c; + fun mat (con,args,mx) = (mat_name_ con, + mk_matT(dtype, map third args, freetvar "t" 1), + Mixfix(escape ("match_" ^ Binding.name_of con), [], Syntax.max_pri)); + fun sel1 (_,sel,typ) = Option.map (fn s => (s,dtype ->> typ,NoSyn)) sel; + fun sel (con,args,mx) = List.mapPartial sel1 args; + fun mk_patT (a,b) = a ->> mk_maybeT b; + fun pat_arg_typ n arg = mk_patT (third arg, freetvar "t" n); + fun pat (con,args,mx) = (pat_name_ con, + (mapn pat_arg_typ 1 args) + ---> + mk_patT (dtype, mk_ctupleT (map (freetvar "t") (1 upto length args))), + Mixfix(escape (Binding.name_of con ^ "_pat"), [], Syntax.max_pri)); + + in + val consts_con = map con cons'; + val consts_dis = map dis cons'; + val consts_mat = map mat cons'; + val consts_pat = map pat cons'; + val consts_sel = List.concat(map sel cons'); + end; + + (* ----- constants concerning induction ------------------------------------- *) + + val const_take = (dbind "_take" , HOLogic.natT-->dtype->>dtype, NoSyn); + val const_finite = (dbind "_finite", dtype-->HOLogic.boolT , NoSyn); + + (* ----- case translation --------------------------------------------------- *) + + local open Syntax in + local + fun c_ast con mx = Constant (Syntax.const_name mx (Binding.name_of con)); + fun expvar n = Variable ("e"^(string_of_int n)); + fun argvar n m _ = Variable ("a"^(string_of_int n)^"_"^ + (string_of_int m)); + fun argvars n args = mapn (argvar n) 1 args; + fun app s (l,r) = mk_appl (Constant s) [l,r]; + val cabs = app "_cabs"; + val capp = app "Rep_CFun"; + fun con1 n (con,args,mx) = Library.foldl capp (c_ast con mx, argvars n args); + fun case1 n (con,args,mx) = app "_case1" (con1 n (con,args,mx), expvar n); + fun arg1 n (con,args,_) = List.foldr cabs (expvar n) (argvars n args); + fun when1 n m = if n = m then arg1 n else K (Constant "UU"); + + fun app_var x = mk_appl (Constant "_variable") [x, Variable "rhs"]; + fun app_pat x = mk_appl (Constant "_pat") [x]; + fun args_list [] = Constant "_noargs" + | args_list xs = foldr1 (app "_args") xs; + in + val case_trans = + ParsePrintRule + (app "_case_syntax" (Variable "x", foldr1 (app "_case2") (mapn case1 1 cons')), + capp (Library.foldl capp (Constant (dnam^"_when"), mapn arg1 1 cons'), Variable "x")); + + fun one_abscon_trans n (con,mx,args) = + ParsePrintRule + (cabs (con1 n (con,mx,args), expvar n), + Library.foldl capp (Constant (dnam^"_when"), mapn (when1 n) 1 cons')); + val abscon_trans = mapn one_abscon_trans 1 cons'; + + fun one_case_trans (con,args,mx) = + let + val cname = c_ast con mx; + val pname = Constant (strip_esc (Binding.name_of con) ^ "_pat"); + val ns = 1 upto length args; + val xs = map (fn n => Variable ("x"^(string_of_int n))) ns; + val ps = map (fn n => Variable ("p"^(string_of_int n))) ns; + val vs = map (fn n => Variable ("v"^(string_of_int n))) ns; + in + [ParseRule (app_pat (Library.foldl capp (cname, xs)), + mk_appl pname (map app_pat xs)), + ParseRule (app_var (Library.foldl capp (cname, xs)), + app_var (args_list xs)), + PrintRule (Library.foldl capp (cname, ListPair.map (app "_match") (ps,vs)), + app "_match" (mk_appl pname ps, args_list vs))] + end; + val Case_trans = List.concat (map one_case_trans cons'); + end; + end; + + in ([const_rep, const_abs, const_when, const_copy] @ + consts_con @ consts_dis @ consts_mat @ consts_pat @ consts_sel @ + [const_take, const_finite], + (case_trans::(abscon_trans @ Case_trans))) + end; (* let *) + +(* ----- putting all the syntax stuff together ------------------------------ *) + +fun add_syntax + (comp_dnam : string) + (eqs' : ((string * typ list) * + (binding * (bool * binding option * typ) list * mixfix) list) list) + (thy'' : theory) = + let + val dtypes = map (Type o fst) eqs'; + val boolT = HOLogic.boolT; + val funprod = foldr1 HOLogic.mk_prodT (map (fn tp => tp ->> tp ) dtypes); + val relprod = foldr1 HOLogic.mk_prodT (map (fn tp => tp --> tp --> boolT) dtypes); + val const_copy = (Binding.name (comp_dnam^"_copy"), funprod ->> funprod, NoSyn); + val const_bisim = (Binding.name (comp_dnam^"_bisim"), relprod --> boolT, NoSyn); + val ctt : ((binding * typ * mixfix) list * ast Syntax.trrule list) list = map (calc_syntax funprod) eqs'; + in thy'' |> ContConsts.add_consts_i (List.concat (map fst ctt) @ + (if length eqs'>1 then [const_copy] else[])@ + [const_bisim]) + |> Sign.add_trrules_i (List.concat(map snd ctt)) + end; (* let *) + +end; (* struct *) diff -r 6da9c2a49fed -r 631546213601 src/HOLCF/Tools/Domain/domain_theorems.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOLCF/Tools/Domain/domain_theorems.ML Tue Jul 21 17:02:18 2009 +0200 @@ -0,0 +1,1053 @@ +(* Title: HOLCF/Tools/Domain/domain_theorems.ML + Author: David von Oheimb + New proofs/tactics by Brian Huffman + +Proof generator for domain command. +*) + +val HOLCF_ss = @{simpset}; + +signature DOMAIN_THEOREMS = +sig + val theorems: Domain_Library.eq * Domain_Library.eq list -> theory -> thm list * theory; + val comp_theorems: bstring * Domain_Library.eq list -> theory -> thm list * theory; + val quiet_mode: bool ref; + val trace_domain: bool ref; +end; + +structure Domain_Theorems :> DOMAIN_THEOREMS = +struct + +val quiet_mode = ref false; +val trace_domain = ref false; + +fun message s = if !quiet_mode then () else writeln s; +fun trace s = if !trace_domain then tracing s else (); + +local + +val adm_impl_admw = @{thm adm_impl_admw}; +val adm_all = @{thm adm_all}; +val adm_conj = @{thm adm_conj}; +val adm_subst = @{thm adm_subst}; +val antisym_less_inverse = @{thm below_antisym_inverse}; +val beta_cfun = @{thm beta_cfun}; +val cfun_arg_cong = @{thm cfun_arg_cong}; +val ch2ch_Rep_CFunL = @{thm ch2ch_Rep_CFunL}; +val ch2ch_Rep_CFunR = @{thm ch2ch_Rep_CFunR}; +val chain_iterate = @{thm chain_iterate}; +val compact_ONE = @{thm compact_ONE}; +val compact_sinl = @{thm compact_sinl}; +val compact_sinr = @{thm compact_sinr}; +val compact_spair = @{thm compact_spair}; +val compact_up = @{thm compact_up}; +val contlub_cfun_arg = @{thm contlub_cfun_arg}; +val contlub_cfun_fun = @{thm contlub_cfun_fun}; +val fix_def2 = @{thm fix_def2}; +val injection_eq = @{thm injection_eq}; +val injection_less = @{thm injection_below}; +val lub_equal = @{thm lub_equal}; +val monofun_cfun_arg = @{thm monofun_cfun_arg}; +val retraction_strict = @{thm retraction_strict}; +val spair_eq = @{thm spair_eq}; +val spair_less = @{thm spair_below}; +val sscase1 = @{thm sscase1}; +val ssplit1 = @{thm ssplit1}; +val strictify1 = @{thm strictify1}; +val wfix_ind = @{thm wfix_ind}; + +val iso_intro = @{thm iso.intro}; +val iso_abs_iso = @{thm iso.abs_iso}; +val iso_rep_iso = @{thm iso.rep_iso}; +val iso_abs_strict = @{thm iso.abs_strict}; +val iso_rep_strict = @{thm iso.rep_strict}; +val iso_abs_defin' = @{thm iso.abs_defin'}; +val iso_rep_defin' = @{thm iso.rep_defin'}; +val iso_abs_defined = @{thm iso.abs_defined}; +val iso_rep_defined = @{thm iso.rep_defined}; +val iso_compact_abs = @{thm iso.compact_abs}; +val iso_compact_rep = @{thm iso.compact_rep}; +val iso_iso_swap = @{thm iso.iso_swap}; + +val exh_start = @{thm exh_start}; +val ex_defined_iffs = @{thms ex_defined_iffs}; +val exh_casedist0 = @{thm exh_casedist0}; +val exh_casedists = @{thms exh_casedists}; + +open Domain_Library; +infixr 0 ===>; +infixr 0 ==>; +infix 0 == ; +infix 1 ===; +infix 1 ~= ; +infix 1 <<; +infix 1 ~<<; +infix 9 ` ; +infix 9 `% ; +infix 9 `%%; +infixr 9 oo; + +(* ----- general proof facilities ------------------------------------------- *) + +fun legacy_infer_term thy t = + let val ctxt = ProofContext.set_mode ProofContext.mode_schematic (ProofContext.init thy) + in singleton (Syntax.check_terms ctxt) (Sign.intern_term thy t) end; + +fun pg'' thy defs t tacs = + let + val t' = legacy_infer_term thy t; + val asms = Logic.strip_imp_prems t'; + val prop = Logic.strip_imp_concl t'; + fun tac {prems, context} = + rewrite_goals_tac defs THEN + EVERY (tacs {prems = map (rewrite_rule defs) prems, context = context}) + in Goal.prove_global thy [] asms prop tac end; + +fun pg' thy defs t tacsf = + let + fun tacs {prems, context} = + if null prems then tacsf context + else cut_facts_tac prems 1 :: tacsf context; + in pg'' thy defs t tacs end; + +fun case_UU_tac ctxt rews i v = + InductTacs.case_tac ctxt (v^"=UU") i THEN + asm_simp_tac (HOLCF_ss addsimps rews) i; + +val chain_tac = + REPEAT_DETERM o resolve_tac + [chain_iterate, ch2ch_Rep_CFunR, ch2ch_Rep_CFunL]; + +(* ----- general proofs ----------------------------------------------------- *) + +val all2E = @{lemma "!x y . P x y ==> (P x y ==> R) ==> R" by simp} + +val dist_eqI = @{lemma "!!x::'a::po. ~ x << y ==> x ~= y" by (blast dest!: below_antisym_inverse)} + +in + +fun theorems (((dname, _), cons) : eq, eqs : eq list) thy = +let + +val _ = message ("Proving isomorphism properties of domain "^dname^" ..."); +val pg = pg' thy; + +(* ----- getting the axioms and definitions --------------------------------- *) + +local + fun ga s dn = PureThy.get_thm thy (dn ^ "." ^ s); +in + val ax_abs_iso = ga "abs_iso" dname; + val ax_rep_iso = ga "rep_iso" dname; + val ax_when_def = ga "when_def" dname; + fun get_def mk_name (con,_) = ga (mk_name con^"_def") dname; + val axs_con_def = map (get_def extern_name) cons; + val axs_dis_def = map (get_def dis_name) cons; + val axs_mat_def = map (get_def mat_name) cons; + val axs_pat_def = map (get_def pat_name) cons; + val axs_sel_def = + let + fun def_of_sel sel = ga (sel^"_def") dname; + fun def_of_arg arg = Option.map def_of_sel (sel_of arg); + fun defs_of_con (_, args) = List.mapPartial def_of_arg args; + in + maps defs_of_con cons + end; + val ax_copy_def = ga "copy_def" dname; +end; (* local *) + +(* ----- theorems concerning the isomorphism -------------------------------- *) + +val dc_abs = %%:(dname^"_abs"); +val dc_rep = %%:(dname^"_rep"); +val dc_copy = %%:(dname^"_copy"); +val x_name = "x"; + +val iso_locale = iso_intro OF [ax_abs_iso, ax_rep_iso]; +val abs_strict = ax_rep_iso RS (allI RS retraction_strict); +val rep_strict = ax_abs_iso RS (allI RS retraction_strict); +val abs_defin' = iso_locale RS iso_abs_defin'; +val rep_defin' = iso_locale RS iso_rep_defin'; +val iso_rews = map standard [ax_abs_iso,ax_rep_iso,abs_strict,rep_strict]; + +(* ----- generating beta reduction rules from definitions-------------------- *) + +val _ = trace " Proving beta reduction rules..."; + +local + fun arglist (Const _ $ Abs (s, _, t)) = + let + val (vars,body) = arglist t; + in (s :: vars, body) end + | arglist t = ([], t); + fun bind_fun vars t = Library.foldr mk_All (vars, t); + fun bound_vars 0 = [] + | bound_vars i = Bound (i-1) :: bound_vars (i - 1); +in + fun appl_of_def def = + let + val (_ $ con $ lam) = concl_of def; + val (vars, rhs) = arglist lam; + val lhs = list_ccomb (con, bound_vars (length vars)); + val appl = bind_fun vars (lhs == rhs); + val cs = ContProc.cont_thms lam; + val betas = map (fn c => mk_meta_eq (c RS beta_cfun)) cs; + in pg (def::betas) appl (K [rtac reflexive_thm 1]) end; +end; + +val _ = trace "Proving when_appl..."; +val when_appl = appl_of_def ax_when_def; +val _ = trace "Proving con_appls..."; +val con_appls = map appl_of_def axs_con_def; + +local + fun arg2typ n arg = + let val t = TVar (("'a", n), pcpoS) + in (n + 1, if is_lazy arg then mk_uT t else t) end; + + fun args2typ n [] = (n, oneT) + | args2typ n [arg] = arg2typ n arg + | args2typ n (arg::args) = + let + val (n1, t1) = arg2typ n arg; + val (n2, t2) = args2typ n1 args + in (n2, mk_sprodT (t1, t2)) end; + + fun cons2typ n [] = (n,oneT) + | cons2typ n [con] = args2typ n (snd con) + | cons2typ n (con::cons) = + let + val (n1, t1) = args2typ n (snd con); + val (n2, t2) = cons2typ n1 cons + in (n2, mk_ssumT (t1, t2)) end; +in + fun cons2ctyp cons = ctyp_of thy (snd (cons2typ 1 cons)); +end; + +local + val iso_swap = iso_locale RS iso_iso_swap; + fun one_con (con, args) = + let + val vns = map vname args; + val eqn = %:x_name === con_app2 con %: vns; + val conj = foldr1 mk_conj (eqn :: map (defined o %:) (nonlazy args)); + in Library.foldr mk_ex (vns, conj) end; + + val conj_assoc = @{thm conj_assoc}; + val exh = foldr1 mk_disj ((%:x_name === UU) :: map one_con cons); + val thm1 = instantiate' [SOME (cons2ctyp cons)] [] exh_start; + val thm2 = rewrite_rule (map mk_meta_eq ex_defined_iffs) thm1; + val thm3 = rewrite_rule [mk_meta_eq @{thm conj_assoc}] thm2; + + (* first 3 rules replace "x = UU \/ P" with "rep$x = UU \/ P" *) + val tacs = [ + rtac disjE 1, + etac (rep_defin' RS disjI1) 2, + etac disjI2 2, + rewrite_goals_tac [mk_meta_eq iso_swap], + rtac thm3 1]; +in + val _ = trace " Proving exhaust..."; + val exhaust = pg con_appls (mk_trp exh) (K tacs); + val _ = trace " Proving casedist..."; + val casedist = + standard (rewrite_rule exh_casedists (exhaust RS exh_casedist0)); +end; + +local + fun bind_fun t = Library.foldr mk_All (when_funs cons, t); + fun bound_fun i _ = Bound (length cons - i); + val when_app = list_ccomb (%%:(dname^"_when"), mapn bound_fun 1 cons); +in + val _ = trace " Proving when_strict..."; + val when_strict = + let + val axs = [when_appl, mk_meta_eq rep_strict]; + val goal = bind_fun (mk_trp (strict when_app)); + val tacs = [resolve_tac [sscase1, ssplit1, strictify1] 1]; + in pg axs goal (K tacs) end; + + val _ = trace " Proving when_apps..."; + val when_apps = + let + fun one_when n (con,args) = + let + val axs = when_appl :: con_appls; + val goal = bind_fun (lift_defined %: (nonlazy args, + mk_trp (when_app`(con_app con args) === + list_ccomb (bound_fun n 0, map %# args)))); + val tacs = [asm_simp_tac (HOLCF_ss addsimps [ax_abs_iso]) 1]; + in pg axs goal (K tacs) end; + in mapn one_when 1 cons end; +end; +val when_rews = when_strict :: when_apps; + +(* ----- theorems concerning the constructors, discriminators and selectors - *) + +local + fun dis_strict (con, _) = + let + val goal = mk_trp (strict (%%:(dis_name con))); + in pg axs_dis_def goal (K [rtac when_strict 1]) end; + + fun dis_app c (con, args) = + let + val lhs = %%:(dis_name c) ` con_app con args; + val rhs = if con = c then TT else FF; + val goal = lift_defined %: (nonlazy args, mk_trp (lhs === rhs)); + val tacs = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1]; + in pg axs_dis_def goal (K tacs) end; + + val _ = trace " Proving dis_apps..."; + val dis_apps = maps (fn (c,_) => map (dis_app c) cons) cons; + + fun dis_defin (con, args) = + let + val goal = defined (%:x_name) ==> defined (%%:(dis_name con) `% x_name); + val tacs = + [rtac casedist 1, + contr_tac 1, + DETERM_UNTIL_SOLVED (CHANGED + (asm_simp_tac (HOLCF_ss addsimps dis_apps) 1))]; + in pg [] goal (K tacs) end; + + val _ = trace " Proving dis_stricts..."; + val dis_stricts = map dis_strict cons; + val _ = trace " Proving dis_defins..."; + val dis_defins = map dis_defin cons; +in + val dis_rews = dis_stricts @ dis_defins @ dis_apps; +end; + +local + fun mat_strict (con, _) = + let + val goal = mk_trp (%%:(mat_name con) ` UU ` %:"rhs" === UU); + val tacs = [asm_simp_tac (HOLCF_ss addsimps [when_strict]) 1]; + in pg axs_mat_def goal (K tacs) end; + + val _ = trace " Proving mat_stricts..."; + val mat_stricts = map mat_strict cons; + + fun one_mat c (con, args) = + let + val lhs = %%:(mat_name c) ` con_app con args ` %:"rhs"; + val rhs = + if con = c + then list_ccomb (%:"rhs", map %# args) + else mk_fail; + val goal = lift_defined %: (nonlazy args, mk_trp (lhs === rhs)); + val tacs = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1]; + in pg axs_mat_def goal (K tacs) end; + + val _ = trace " Proving mat_apps..."; + val mat_apps = + maps (fn (c,_) => map (one_mat c) cons) cons; +in + val mat_rews = mat_stricts @ mat_apps; +end; + +local + fun ps args = mapn (fn n => fn _ => %:("pat" ^ string_of_int n)) 1 args; + + fun pat_lhs (con,args) = mk_branch (list_comb (%%:(pat_name con), ps args)); + + fun pat_rhs (con,[]) = mk_return ((%:"rhs") ` HOLogic.unit) + | pat_rhs (con,args) = + (mk_branch (mk_ctuple_pat (ps args))) + `(%:"rhs")`(mk_ctuple (map %# args)); + + fun pat_strict c = + let + val axs = @{thm branch_def} :: axs_pat_def; + val goal = mk_trp (strict (pat_lhs c ` (%:"rhs"))); + val tacs = [simp_tac (HOLCF_ss addsimps [when_strict]) 1]; + in pg axs goal (K tacs) end; + + fun pat_app c (con, args) = + let + val axs = @{thm branch_def} :: axs_pat_def; + val lhs = (pat_lhs c)`(%:"rhs")`(con_app con args); + val rhs = if con = fst c then pat_rhs c else mk_fail; + val goal = lift_defined %: (nonlazy args, mk_trp (lhs === rhs)); + val tacs = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1]; + in pg axs goal (K tacs) end; + + val _ = trace " Proving pat_stricts..."; + val pat_stricts = map pat_strict cons; + val _ = trace " Proving pat_apps..."; + val pat_apps = maps (fn c => map (pat_app c) cons) cons; +in + val pat_rews = pat_stricts @ pat_apps; +end; + +local + fun con_strict (con, args) = + let + val rules = abs_strict :: @{thms con_strict_rules}; + fun one_strict vn = + let + fun f arg = if vname arg = vn then UU else %# arg; + val goal = mk_trp (con_app2 con f args === UU); + val tacs = [simp_tac (HOL_basic_ss addsimps rules) 1]; + in pg con_appls goal (K tacs) end; + in map one_strict (nonlazy args) end; + + fun con_defin (con, args) = + let + fun iff_disj (t, []) = HOLogic.mk_not t + | iff_disj (t, ts) = t === foldr1 HOLogic.mk_disj ts; + val lhs = con_app con args === UU; + val rhss = map (fn x => %:x === UU) (nonlazy args); + val goal = mk_trp (iff_disj (lhs, rhss)); + val rule1 = iso_locale RS @{thm iso.abs_defined_iff}; + val rules = rule1 :: @{thms con_defined_iff_rules}; + val tacs = [simp_tac (HOL_ss addsimps rules) 1]; + in pg con_appls goal (K tacs) end; +in + val _ = trace " Proving con_stricts..."; + val con_stricts = maps con_strict cons; + val _ = trace " Proving con_defins..."; + val con_defins = map con_defin cons; + val con_rews = con_stricts @ con_defins; +end; + +local + val rules = + [compact_sinl, compact_sinr, compact_spair, compact_up, compact_ONE]; + fun con_compact (con, args) = + let + val concl = mk_trp (mk_compact (con_app con args)); + val goal = lift (fn x => mk_compact (%#x)) (args, concl); + val tacs = [ + rtac (iso_locale RS iso_compact_abs) 1, + REPEAT (resolve_tac rules 1 ORELSE atac 1)]; + in pg con_appls goal (K tacs) end; +in + val _ = trace " Proving con_compacts..."; + val con_compacts = map con_compact cons; +end; + +local + fun one_sel sel = + pg axs_sel_def (mk_trp (strict (%%:sel))) + (K [simp_tac (HOLCF_ss addsimps when_rews) 1]); + + fun sel_strict (_, args) = + List.mapPartial (Option.map one_sel o sel_of) args; +in + val _ = trace " Proving sel_stricts..."; + val sel_stricts = maps sel_strict cons; +end; + +local + fun sel_app_same c n sel (con, args) = + let + val nlas = nonlazy args; + val vns = map vname args; + val vnn = List.nth (vns, n); + val nlas' = List.filter (fn v => v <> vnn) nlas; + val lhs = (%%:sel)`(con_app con args); + val goal = lift_defined %: (nlas', mk_trp (lhs === %:vnn)); + fun tacs1 ctxt = + if vnn mem nlas + then [case_UU_tac ctxt (when_rews @ con_stricts) 1 vnn] + else []; + val tacs2 = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1]; + in pg axs_sel_def goal (fn ctxt => (tacs1 ctxt @ tacs2)) end; + + fun sel_app_diff c n sel (con, args) = + let + val nlas = nonlazy args; + val goal = mk_trp (%%:sel ` con_app con args === UU); + fun tacs1 ctxt = map (case_UU_tac ctxt (when_rews @ con_stricts) 1) nlas; + val tacs2 = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1]; + in pg axs_sel_def goal (fn ctxt => (tacs1 ctxt @ tacs2)) end; + + fun sel_app c n sel (con, args) = + if con = c + then sel_app_same c n sel (con, args) + else sel_app_diff c n sel (con, args); + + fun one_sel c n sel = map (sel_app c n sel) cons; + fun one_sel' c n arg = Option.map (one_sel c n) (sel_of arg); + fun one_con (c, args) = + flat (map_filter I (mapn (one_sel' c) 0 args)); +in + val _ = trace " Proving sel_apps..."; + val sel_apps = maps one_con cons; +end; + +local + fun sel_defin sel = + let + val goal = defined (%:x_name) ==> defined (%%:sel`%x_name); + val tacs = [ + rtac casedist 1, + contr_tac 1, + DETERM_UNTIL_SOLVED (CHANGED + (asm_simp_tac (HOLCF_ss addsimps sel_apps) 1))]; + in pg [] goal (K tacs) end; +in + val _ = trace " Proving sel_defins..."; + val sel_defins = + if length cons = 1 + then List.mapPartial (fn arg => Option.map sel_defin (sel_of arg)) + (filter_out is_lazy (snd (hd cons))) + else []; +end; + +val sel_rews = sel_stricts @ sel_defins @ sel_apps; + +val _ = trace " Proving dist_les..."; +val distincts_le = + let + fun dist (con1, args1) (con2, args2) = + let + val goal = lift_defined %: (nonlazy args1, + mk_trp (con_app con1 args1 ~<< con_app con2 args2)); + fun tacs ctxt = [ + rtac @{thm rev_contrapos} 1, + eres_inst_tac ctxt [(("f", 0), dis_name con1)] monofun_cfun_arg 1] + @ map (case_UU_tac ctxt (con_stricts @ dis_rews) 1) (nonlazy args2) + @ [asm_simp_tac (HOLCF_ss addsimps dis_rews) 1]; + in pg [] goal tacs end; + + fun distinct (con1, args1) (con2, args2) = + let + val arg1 = (con1, args1); + val arg2 = + (con2, ListPair.map (fn (arg,vn) => upd_vname (K vn) arg) + (args2, Name.variant_list (map vname args1) (map vname args2))); + in [dist arg1 arg2, dist arg2 arg1] end; + fun distincts [] = [] + | distincts (c::cs) = (map (distinct c) cs) :: distincts cs; + in distincts cons end; +val dist_les = flat (flat distincts_le); + +val _ = trace " Proving dist_eqs..."; +val dist_eqs = + let + fun distinct (_,args1) ((_,args2), leqs) = + let + val (le1,le2) = (hd leqs, hd(tl leqs)); + val (eq1,eq2) = (le1 RS dist_eqI, le2 RS dist_eqI) + in + if nonlazy args1 = [] then [eq1, eq1 RS not_sym] else + if nonlazy args2 = [] then [eq2, eq2 RS not_sym] else + [eq1, eq2] + end; + fun distincts [] = [] + | distincts ((c,leqs)::cs) = + flat + (ListPair.map (distinct c) ((map #1 cs),leqs)) @ + distincts cs; + in map standard (distincts (cons ~~ distincts_le)) end; + +local + fun pgterm rel con args = + let + fun append s = upd_vname (fn v => v^s); + val (largs, rargs) = (args, map (append "'") args); + val concl = + foldr1 mk_conj (ListPair.map rel (map %# largs, map %# rargs)); + val prem = rel (con_app con largs, con_app con rargs); + val sargs = case largs of [_] => [] | _ => nonlazy args; + val prop = lift_defined %: (sargs, mk_trp (prem === concl)); + in pg con_appls prop end; + val cons' = List.filter (fn (_,args) => args<>[]) cons; +in + val _ = trace " Proving inverts..."; + val inverts = + let + val abs_less = ax_abs_iso RS (allI RS injection_less); + val tacs = + [asm_full_simp_tac (HOLCF_ss addsimps [abs_less, spair_less]) 1]; + in map (fn (con, args) => pgterm (op <<) con args (K tacs)) cons' end; + + val _ = trace " Proving injects..."; + val injects = + let + val abs_eq = ax_abs_iso RS (allI RS injection_eq); + val tacs = [asm_full_simp_tac (HOLCF_ss addsimps [abs_eq, spair_eq]) 1]; + in map (fn (con, args) => pgterm (op ===) con args (K tacs)) cons' end; +end; + +(* ----- theorems concerning one induction step ----------------------------- *) + +val copy_strict = + let + val _ = trace " Proving copy_strict..."; + val goal = mk_trp (strict (dc_copy `% "f")); + val rules = [abs_strict, rep_strict] @ @{thms domain_fun_stricts}; + val tacs = [asm_simp_tac (HOLCF_ss addsimps rules) 1]; + in pg [ax_copy_def] goal (K tacs) end; + +local + fun copy_app (con, args) = + let + val lhs = dc_copy`%"f"`(con_app con args); + fun one_rhs arg = + if DatatypeAux.is_rec_type (dtyp_of arg) + then Domain_Axioms.copy_of_dtyp (cproj (%:"f") eqs) (dtyp_of arg) ` (%# arg) + else (%# arg); + val rhs = con_app2 con one_rhs args; + val goal = lift_defined %: (nonlazy_rec args, mk_trp (lhs === rhs)); + val args' = List.filter (fn a => not (is_rec a orelse is_lazy a)) args; + val stricts = abs_strict :: rep_strict :: @{thms domain_fun_stricts}; + fun tacs1 ctxt = map (case_UU_tac ctxt stricts 1 o vname) args'; + val rules = [ax_abs_iso] @ @{thms domain_fun_simps}; + val tacs2 = [asm_simp_tac (HOLCF_ss addsimps rules) 1]; + in pg (ax_copy_def::con_appls) goal (fn ctxt => (tacs1 ctxt @ tacs2)) end; +in + val _ = trace " Proving copy_apps..."; + val copy_apps = map copy_app cons; +end; + +local + fun one_strict (con, args) = + let + val goal = mk_trp (dc_copy`UU`(con_app con args) === UU); + val rews = copy_strict :: copy_apps @ con_rews; + fun tacs ctxt = map (case_UU_tac ctxt rews 1) (nonlazy args) @ + [asm_simp_tac (HOLCF_ss addsimps rews) 1]; + in pg [] goal tacs end; + + fun has_nonlazy_rec (_, args) = exists is_nonlazy_rec args; +in + val _ = trace " Proving copy_stricts..."; + val copy_stricts = map one_strict (List.filter has_nonlazy_rec cons); +end; + +val copy_rews = copy_strict :: copy_apps @ copy_stricts; + +in + thy + |> Sign.add_path (Long_Name.base_name dname) + |> snd o PureThy.add_thmss [ + ((Binding.name "iso_rews" , iso_rews ), [Simplifier.simp_add]), + ((Binding.name "exhaust" , [exhaust] ), []), + ((Binding.name "casedist" , [casedist] ), [Induct.cases_type dname]), + ((Binding.name "when_rews" , when_rews ), [Simplifier.simp_add]), + ((Binding.name "compacts" , con_compacts), [Simplifier.simp_add]), + ((Binding.name "con_rews" , con_rews ), [Simplifier.simp_add]), + ((Binding.name "sel_rews" , sel_rews ), [Simplifier.simp_add]), + ((Binding.name "dis_rews" , dis_rews ), [Simplifier.simp_add]), + ((Binding.name "pat_rews" , pat_rews ), [Simplifier.simp_add]), + ((Binding.name "dist_les" , dist_les ), [Simplifier.simp_add]), + ((Binding.name "dist_eqs" , dist_eqs ), [Simplifier.simp_add]), + ((Binding.name "inverts" , inverts ), [Simplifier.simp_add]), + ((Binding.name "injects" , injects ), [Simplifier.simp_add]), + ((Binding.name "copy_rews" , copy_rews ), [Simplifier.simp_add]), + ((Binding.name "match_rews", mat_rews ), [Simplifier.simp_add])] + |> Sign.parent_path + |> pair (iso_rews @ when_rews @ con_rews @ sel_rews @ dis_rews @ + pat_rews @ dist_les @ dist_eqs @ copy_rews) +end; (* let *) + +fun comp_theorems (comp_dnam, eqs: eq list) thy = +let +val global_ctxt = ProofContext.init thy; + +val dnames = map (fst o fst) eqs; +val conss = map snd eqs; +val comp_dname = Sign.full_bname thy comp_dnam; + +val _ = message ("Proving induction properties of domain "^comp_dname^" ..."); +val pg = pg' thy; + +(* ----- getting the composite axiom and definitions ------------------------ *) + +local + fun ga s dn = PureThy.get_thm thy (dn ^ "." ^ s); +in + val axs_reach = map (ga "reach" ) dnames; + val axs_take_def = map (ga "take_def" ) dnames; + val axs_finite_def = map (ga "finite_def") dnames; + val ax_copy2_def = ga "copy_def" comp_dnam; + val ax_bisim_def = ga "bisim_def" comp_dnam; +end; + +local + fun gt s dn = PureThy.get_thm thy (dn ^ "." ^ s); + fun gts s dn = PureThy.get_thms thy (dn ^ "." ^ s); +in + val cases = map (gt "casedist" ) dnames; + val con_rews = maps (gts "con_rews" ) dnames; + val copy_rews = maps (gts "copy_rews") dnames; +end; + +fun dc_take dn = %%:(dn^"_take"); +val x_name = idx_name dnames "x"; +val P_name = idx_name dnames "P"; +val n_eqs = length eqs; + +(* ----- theorems concerning finite approximation and finite induction ------ *) + +local + val iterate_Cprod_ss = simpset_of @{theory Fix}; + val copy_con_rews = copy_rews @ con_rews; + val copy_take_defs = + (if n_eqs = 1 then [] else [ax_copy2_def]) @ axs_take_def; + val _ = trace " Proving take_stricts..."; + val take_stricts = + let + fun one_eq ((dn, args), _) = strict (dc_take dn $ %:"n"); + val goal = mk_trp (foldr1 mk_conj (map one_eq eqs)); + fun tacs ctxt = [ + InductTacs.induct_tac ctxt [[SOME "n"]] 1, + simp_tac iterate_Cprod_ss 1, + asm_simp_tac (iterate_Cprod_ss addsimps copy_rews) 1]; + in pg copy_take_defs goal tacs end; + + val take_stricts' = rewrite_rule copy_take_defs take_stricts; + fun take_0 n dn = + let + val goal = mk_trp ((dc_take dn $ %%:"HOL.zero") `% x_name n === UU); + in pg axs_take_def goal (K [simp_tac iterate_Cprod_ss 1]) end; + val take_0s = mapn take_0 1 dnames; + fun c_UU_tac ctxt = case_UU_tac ctxt (take_stricts'::copy_con_rews) 1; + val _ = trace " Proving take_apps..."; + val take_apps = + let + fun mk_eqn dn (con, args) = + let + fun mk_take n = dc_take (List.nth (dnames, n)) $ %:"n"; + fun one_rhs arg = + if DatatypeAux.is_rec_type (dtyp_of arg) + then Domain_Axioms.copy_of_dtyp mk_take (dtyp_of arg) ` (%# arg) + else (%# arg); + val lhs = (dc_take dn $ (%%:"Suc" $ %:"n"))`(con_app con args); + val rhs = con_app2 con one_rhs args; + in Library.foldr mk_all (map vname args, lhs === rhs) end; + fun mk_eqns ((dn, _), cons) = map (mk_eqn dn) cons; + val goal = mk_trp (foldr1 mk_conj (maps mk_eqns eqs)); + val simps = List.filter (has_fewer_prems 1) copy_rews; + fun con_tac ctxt (con, args) = + if nonlazy_rec args = [] + then all_tac + else EVERY (map (c_UU_tac ctxt) (nonlazy_rec args)) THEN + asm_full_simp_tac (HOLCF_ss addsimps copy_rews) 1; + fun eq_tacs ctxt ((dn, _), cons) = map (con_tac ctxt) cons; + fun tacs ctxt = + simp_tac iterate_Cprod_ss 1 :: + InductTacs.induct_tac ctxt [[SOME "n"]] 1 :: + simp_tac (iterate_Cprod_ss addsimps copy_con_rews) 1 :: + asm_full_simp_tac (HOLCF_ss addsimps simps) 1 :: + TRY (safe_tac HOL_cs) :: + maps (eq_tacs ctxt) eqs; + in pg copy_take_defs goal tacs end; +in + val take_rews = map standard + (atomize global_ctxt take_stricts @ take_0s @ atomize global_ctxt take_apps); +end; (* local *) + +local + fun one_con p (con,args) = + let + fun ind_hyp arg = %:(P_name (1 + rec_of arg)) $ bound_arg args arg; + val t1 = mk_trp (%:p $ con_app2 con (bound_arg args) args); + val t2 = lift ind_hyp (List.filter is_rec args, t1); + val t3 = lift_defined (bound_arg (map vname args)) (nonlazy args, t2); + in Library.foldr mk_All (map vname args, t3) end; + + fun one_eq ((p, cons), concl) = + mk_trp (%:p $ UU) ===> Logic.list_implies (map (one_con p) cons, concl); + + fun ind_term concf = Library.foldr one_eq + (mapn (fn n => fn x => (P_name n, x)) 1 conss, + mk_trp (foldr1 mk_conj (mapn concf 1 dnames))); + val take_ss = HOL_ss addsimps take_rews; + fun quant_tac ctxt i = EVERY + (mapn (fn n => fn _ => res_inst_tac ctxt [(("x", 0), x_name n)] spec i) 1 dnames); + + fun ind_prems_tac prems = EVERY + (maps (fn cons => + (resolve_tac prems 1 :: + maps (fn (_,args) => + resolve_tac prems 1 :: + map (K(atac 1)) (nonlazy args) @ + map (K(atac 1)) (List.filter is_rec args)) + cons)) + conss); + local + (* check whether every/exists constructor of the n-th part of the equation: + it has a possibly indirectly recursive argument that isn't/is possibly + indirectly lazy *) + fun rec_to quant nfn rfn ns lazy_rec (n,cons) = quant (exists (fn arg => + is_rec arg andalso not(rec_of arg mem ns) andalso + ((rec_of arg = n andalso nfn(lazy_rec orelse is_lazy arg)) orelse + rec_of arg <> n andalso rec_to quant nfn rfn (rec_of arg::ns) + (lazy_rec orelse is_lazy arg) (n, (List.nth(conss,rec_of arg)))) + ) o snd) cons; + fun all_rec_to ns = rec_to forall not all_rec_to ns; + fun warn (n,cons) = + if all_rec_to [] false (n,cons) + then (warning ("domain "^List.nth(dnames,n)^" is empty!"); true) + else false; + fun lazy_rec_to ns = rec_to exists I lazy_rec_to ns; + + in + val n__eqs = mapn (fn n => fn (_,cons) => (n,cons)) 0 eqs; + val is_emptys = map warn n__eqs; + val is_finite = forall (not o lazy_rec_to [] false) n__eqs; + end; +in (* local *) + val _ = trace " Proving finite_ind..."; + val finite_ind = + let + fun concf n dn = %:(P_name n) $ (dc_take dn $ %:"n" `%(x_name n)); + val goal = ind_term concf; + + fun tacf {prems, context} = + let + val tacs1 = [ + quant_tac context 1, + simp_tac HOL_ss 1, + InductTacs.induct_tac context [[SOME "n"]] 1, + simp_tac (take_ss addsimps prems) 1, + TRY (safe_tac HOL_cs)]; + fun arg_tac arg = + case_UU_tac context (prems @ con_rews) 1 + (List.nth (dnames, rec_of arg) ^ "_take n$" ^ vname arg); + fun con_tacs (con, args) = + asm_simp_tac take_ss 1 :: + map arg_tac (List.filter is_nonlazy_rec args) @ + [resolve_tac prems 1] @ + map (K (atac 1)) (nonlazy args) @ + map (K (etac spec 1)) (List.filter is_rec args); + fun cases_tacs (cons, cases) = + res_inst_tac context [(("x", 0), "x")] cases 1 :: + asm_simp_tac (take_ss addsimps prems) 1 :: + maps con_tacs cons; + in + tacs1 @ maps cases_tacs (conss ~~ cases) + end; + in pg'' thy [] goal tacf + handle ERROR _ => (warning "Proof of finite_ind failed."; TrueI) + end; + + val _ = trace " Proving take_lemmas..."; + val take_lemmas = + let + fun take_lemma n (dn, ax_reach) = + let + val lhs = dc_take dn $ Bound 0 `%(x_name n); + val rhs = dc_take dn $ Bound 0 `%(x_name n^"'"); + val concl = mk_trp (%:(x_name n) === %:(x_name n^"'")); + val goal = mk_All ("n", mk_trp (lhs === rhs)) ===> concl; + fun tacf {prems, context} = [ + res_inst_tac context [(("t", 0), x_name n )] (ax_reach RS subst) 1, + res_inst_tac context [(("t", 0), x_name n^"'")] (ax_reach RS subst) 1, + stac fix_def2 1, + REPEAT (CHANGED + (rtac (contlub_cfun_arg RS ssubst) 1 THEN chain_tac 1)), + stac contlub_cfun_fun 1, + stac contlub_cfun_fun 2, + rtac lub_equal 3, + chain_tac 1, + rtac allI 1, + resolve_tac prems 1]; + in pg'' thy axs_take_def goal tacf end; + in mapn take_lemma 1 (dnames ~~ axs_reach) end; + +(* ----- theorems concerning finiteness and induction ----------------------- *) + + val _ = trace " Proving finites, ind..."; + val (finites, ind) = + ( + if is_finite + then (* finite case *) + let + fun take_enough dn = mk_ex ("n",dc_take dn $ Bound 0 ` %:"x" === %:"x"); + fun dname_lemma dn = + let + val prem1 = mk_trp (defined (%:"x")); + val disj1 = mk_all ("n", dc_take dn $ Bound 0 ` %:"x" === UU); + val prem2 = mk_trp (mk_disj (disj1, take_enough dn)); + val concl = mk_trp (take_enough dn); + val goal = prem1 ===> prem2 ===> concl; + val tacs = [ + etac disjE 1, + etac notE 1, + resolve_tac take_lemmas 1, + asm_simp_tac take_ss 1, + atac 1]; + in pg [] goal (K tacs) end; + val _ = trace " Proving finite_lemmas1a"; + val finite_lemmas1a = map dname_lemma dnames; + + val _ = trace " Proving finite_lemma1b"; + val finite_lemma1b = + let + fun mk_eqn n ((dn, args), _) = + let + val disj1 = dc_take dn $ Bound 1 ` Bound 0 === UU; + val disj2 = dc_take dn $ Bound 1 ` Bound 0 === Bound 0; + in + mk_constrainall + (x_name n, Type (dn,args), mk_disj (disj1, disj2)) + end; + val goal = + mk_trp (mk_all ("n", foldr1 mk_conj (mapn mk_eqn 1 eqs))); + fun arg_tacs ctxt vn = [ + eres_inst_tac ctxt [(("x", 0), vn)] all_dupE 1, + etac disjE 1, + asm_simp_tac (HOL_ss addsimps con_rews) 1, + asm_simp_tac take_ss 1]; + fun con_tacs ctxt (con, args) = + asm_simp_tac take_ss 1 :: + maps (arg_tacs ctxt) (nonlazy_rec args); + fun foo_tacs ctxt n (cons, cases) = + simp_tac take_ss 1 :: + rtac allI 1 :: + res_inst_tac ctxt [(("x", 0), x_name n)] cases 1 :: + asm_simp_tac take_ss 1 :: + maps (con_tacs ctxt) cons; + fun tacs ctxt = + rtac allI 1 :: + InductTacs.induct_tac ctxt [[SOME "n"]] 1 :: + simp_tac take_ss 1 :: + TRY (safe_tac (empty_cs addSEs [conjE] addSIs [conjI])) :: + flat (mapn (foo_tacs ctxt) 1 (conss ~~ cases)); + in pg [] goal tacs end; + + fun one_finite (dn, l1b) = + let + val goal = mk_trp (%%:(dn^"_finite") $ %:"x"); + fun tacs ctxt = [ + case_UU_tac ctxt take_rews 1 "x", + eresolve_tac finite_lemmas1a 1, + step_tac HOL_cs 1, + step_tac HOL_cs 1, + cut_facts_tac [l1b] 1, + fast_tac HOL_cs 1]; + in pg axs_finite_def goal tacs end; + + val _ = trace " Proving finites"; + val finites = map one_finite (dnames ~~ atomize global_ctxt finite_lemma1b); + val _ = trace " Proving ind"; + val ind = + let + fun concf n dn = %:(P_name n) $ %:(x_name n); + fun tacf {prems, context} = + let + fun finite_tacs (finite, fin_ind) = [ + rtac(rewrite_rule axs_finite_def finite RS exE)1, + etac subst 1, + rtac fin_ind 1, + ind_prems_tac prems]; + in + TRY (safe_tac HOL_cs) :: + maps finite_tacs (finites ~~ atomize global_ctxt finite_ind) + end; + in pg'' thy [] (ind_term concf) tacf end; + in (finites, ind) end (* let *) + + else (* infinite case *) + let + fun one_finite n dn = + read_instantiate global_ctxt [(("P", 0), dn ^ "_finite " ^ x_name n)] excluded_middle; + val finites = mapn one_finite 1 dnames; + + val goal = + let + fun one_adm n _ = mk_trp (mk_adm (%:(P_name n))); + fun concf n dn = %:(P_name n) $ %:(x_name n); + in Logic.list_implies (mapn one_adm 1 dnames, ind_term concf) end; + fun tacf {prems, context} = + map (fn ax_reach => rtac (ax_reach RS subst) 1) axs_reach @ [ + quant_tac context 1, + rtac (adm_impl_admw RS wfix_ind) 1, + REPEAT_DETERM (rtac adm_all 1), + REPEAT_DETERM ( + TRY (rtac adm_conj 1) THEN + rtac adm_subst 1 THEN + cont_tacR 1 THEN resolve_tac prems 1), + strip_tac 1, + rtac (rewrite_rule axs_take_def finite_ind) 1, + ind_prems_tac prems]; + val ind = (pg'' thy [] goal tacf + handle ERROR _ => + (warning "Cannot prove infinite induction rule"; refl)); + in (finites, ind) end + ) + handle THM _ => + (warning "Induction proofs failed (THM raised)."; ([], TrueI)) + | ERROR _ => + (warning "Induction proofs failed (ERROR raised)."; ([], TrueI)); + + +end; (* local *) + +(* ----- theorem concerning coinduction ------------------------------------- *) + +local + val xs = mapn (fn n => K (x_name n)) 1 dnames; + fun bnd_arg n i = Bound(2*(n_eqs - n)-i-1); + val take_ss = HOL_ss addsimps take_rews; + val sproj = prj (fn s => K("fst("^s^")")) (fn s => K("snd("^s^")")); + val _ = trace " Proving coind_lemma..."; + val coind_lemma = + let + fun mk_prj n _ = proj (%:"R") eqs n $ bnd_arg n 0 $ bnd_arg n 1; + fun mk_eqn n dn = + (dc_take dn $ %:"n" ` bnd_arg n 0) === + (dc_take dn $ %:"n" ` bnd_arg n 1); + fun mk_all2 (x,t) = mk_all (x, mk_all (x^"'", t)); + val goal = + mk_trp (mk_imp (%%:(comp_dname^"_bisim") $ %:"R", + Library.foldr mk_all2 (xs, + Library.foldr mk_imp (mapn mk_prj 0 dnames, + foldr1 mk_conj (mapn mk_eqn 0 dnames))))); + fun x_tacs ctxt n x = [ + rotate_tac (n+1) 1, + etac all2E 1, + eres_inst_tac ctxt [(("P", 1), sproj "R" eqs n^" "^x^" "^x^"'")] (mp RS disjE) 1, + TRY (safe_tac HOL_cs), + REPEAT (CHANGED (asm_simp_tac take_ss 1))]; + fun tacs ctxt = [ + rtac impI 1, + InductTacs.induct_tac ctxt [[SOME "n"]] 1, + simp_tac take_ss 1, + safe_tac HOL_cs] @ + flat (mapn (x_tacs ctxt) 0 xs); + in pg [ax_bisim_def] goal tacs end; +in + val _ = trace " Proving coind..."; + val coind = + let + fun mk_prj n x = mk_trp (proj (%:"R") eqs n $ %:x $ %:(x^"'")); + fun mk_eqn x = %:x === %:(x^"'"); + val goal = + mk_trp (%%:(comp_dname^"_bisim") $ %:"R") ===> + Logic.list_implies (mapn mk_prj 0 xs, + mk_trp (foldr1 mk_conj (map mk_eqn xs))); + val tacs = + TRY (safe_tac HOL_cs) :: + maps (fn take_lemma => [ + rtac take_lemma 1, + cut_facts_tac [coind_lemma] 1, + fast_tac HOL_cs 1]) + take_lemmas; + in pg [] goal (K tacs) end; +end; (* local *) + +val inducts = ProjectRule.projections (ProofContext.init thy) ind; +fun ind_rule (dname, rule) = ((Binding.empty, [rule]), [Induct.induct_type dname]); +val induct_failed = (Thm.prop_of ind = Thm.prop_of TrueI); + +in thy |> Sign.add_path comp_dnam + |> snd o PureThy.add_thmss [ + ((Binding.name "take_rews" , take_rews ), [Simplifier.simp_add]), + ((Binding.name "take_lemmas", take_lemmas ), []), + ((Binding.name "finites" , finites ), []), + ((Binding.name "finite_ind" , [finite_ind]), []), + ((Binding.name "ind" , [ind] ), []), + ((Binding.name "coind" , [coind] ), [])] + |> (if induct_failed then I + else snd o PureThy.add_thmss (map ind_rule (dnames ~~ inducts))) + |> Sign.parent_path |> pair take_rews +end; (* let *) +end; (* local *) +end; (* struct *) diff -r 6da9c2a49fed -r 631546213601 src/HOLCF/Tools/domain/domain_axioms.ML --- a/src/HOLCF/Tools/domain/domain_axioms.ML Tue Jul 21 14:08:58 2009 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,235 +0,0 @@ -(* Title: HOLCF/Tools/domain/domain_axioms.ML - Author: David von Oheimb - -Syntax generator for domain command. -*) - -signature DOMAIN_AXIOMS = -sig - val copy_of_dtyp : (int -> term) -> Datatype.dtyp -> term - - val calc_axioms : - string -> Domain_Library.eq list -> int -> Domain_Library.eq -> - string * (string * term) list * (string * term) list - - val add_axioms : - bstring -> Domain_Library.eq list -> theory -> theory -end; - - -structure Domain_Axioms :> DOMAIN_AXIOMS = -struct - -open Domain_Library; - -infixr 0 ===>;infixr 0 ==>;infix 0 == ; -infix 1 ===; infix 1 ~= ; infix 1 <<; infix 1 ~<<; -infix 9 ` ; infix 9 `% ; infix 9 `%%; infixr 9 oo; - -(* FIXME: use theory data for this *) -val copy_tab : string Symtab.table = - Symtab.make [(@{type_name "->"}, @{const_name "cfun_fun"}), - (@{type_name "++"}, @{const_name "ssum_fun"}), - (@{type_name "**"}, @{const_name "sprod_fun"}), - (@{type_name "*"}, @{const_name "cprod_fun"}), - (@{type_name "u"}, @{const_name "u_fun"})]; - -fun copy_of_dtyp r dt = if DatatypeAux.is_rec_type dt then copy r dt else ID -and copy r (DatatypeAux.DtRec i) = r i - | copy r (DatatypeAux.DtTFree a) = ID - | copy r (DatatypeAux.DtType (c, ds)) = - case Symtab.lookup copy_tab c of - SOME f => list_ccomb (%%:f, map (copy_of_dtyp r) ds) - | NONE => (warning ("copy_of_dtyp: unknown type constructor " ^ c); ID); - -fun calc_axioms - (comp_dname : string) - (eqs : eq list) - (n : int) - (eqn as ((dname,_),cons) : eq) - : string * (string * term) list * (string * term) list = - let - - (* ----- axioms and definitions concerning the isomorphism ------------------ *) - - val dc_abs = %%:(dname^"_abs"); - val dc_rep = %%:(dname^"_rep"); - val x_name'= "x"; - val x_name = idx_name eqs x_name' (n+1); - val dnam = Long_Name.base_name dname; - - val abs_iso_ax = ("abs_iso", mk_trp(dc_rep`(dc_abs`%x_name') === %:x_name')); - val rep_iso_ax = ("rep_iso", mk_trp(dc_abs`(dc_rep`%x_name') === %:x_name')); - - val when_def = ("when_def",%%:(dname^"_when") == - List.foldr (uncurry /\ ) (/\x_name'((when_body cons (fn (x,y) => - Bound(1+length cons+x-y)))`(dc_rep`Bound 0))) (when_funs cons)); - - val copy_def = - let fun r i = cproj (Bound 0) eqs i; - in ("copy_def", %%:(dname^"_copy") == - /\ "f" (dc_abs oo (copy_of_dtyp r (dtyp_of_eq eqn)) oo dc_rep)) end; - - (* -- definitions concerning the constructors, discriminators and selectors - *) - - fun con_def m n (_,args) = let - fun idxs z x arg = (if is_lazy arg then mk_up else I) (Bound(z-x)); - fun parms vs = mk_stuple (mapn (idxs(length vs)) 1 vs); - fun inj y 1 _ = y - | inj y _ 0 = mk_sinl y - | inj y i j = mk_sinr (inj y (i-1) (j-1)); - in List.foldr /\# (dc_abs`(inj (parms args) m n)) args end; - - val con_defs = mapn (fn n => fn (con,args) => - (extern_name con ^"_def", %%:con == con_def (length cons) n (con,args))) 0 cons; - - val dis_defs = let - fun ddef (con,_) = (dis_name con ^"_def",%%:(dis_name con) == - list_ccomb(%%:(dname^"_when"),map - (fn (con',args) => (List.foldr /\# - (if con'=con then TT else FF) args)) cons)) - in map ddef cons end; - - val mat_defs = - let - fun mdef (con,_) = - let - val k = Bound 0 - val x = Bound 1 - fun one_con (con', args') = - if con'=con then k else List.foldr /\# mk_fail args' - val w = list_ccomb(%%:(dname^"_when"), map one_con cons) - val rhs = /\ "x" (/\ "k" (w ` x)) - in (mat_name con ^"_def", %%:(mat_name con) == rhs) end - in map mdef cons end; - - val pat_defs = - let - fun pdef (con,args) = - let - val ps = mapn (fn n => fn _ => %:("pat" ^ string_of_int n)) 1 args; - val xs = map (bound_arg args) args; - val r = Bound (length args); - val rhs = case args of [] => mk_return HOLogic.unit - | _ => mk_ctuple_pat ps ` mk_ctuple xs; - fun one_con (con',args') = List.foldr /\# (if con'=con then rhs else mk_fail) args'; - in (pat_name con ^"_def", list_comb (%%:(pat_name con), ps) == - list_ccomb(%%:(dname^"_when"), map one_con cons)) - end - in map pdef cons end; - - val sel_defs = let - fun sdef con n arg = Option.map (fn sel => (sel^"_def",%%:sel == - list_ccomb(%%:(dname^"_when"),map - (fn (con',args) => if con'<>con then UU else - List.foldr /\# (Bound (length args - n)) args) cons))) (sel_of arg); - in List.mapPartial I (List.concat(map (fn (con,args) => mapn (sdef con) 1 args) cons)) end; - - - (* ----- axiom and definitions concerning induction ------------------------- *) - - val reach_ax = ("reach", mk_trp(cproj (mk_fix (%%:(comp_dname^"_copy"))) eqs n - `%x_name === %:x_name)); - val take_def = - ("take_def", - %%:(dname^"_take") == - mk_lam("n",cproj - (mk_iterate (Bound 0, %%:(comp_dname^"_copy"), UU)) eqs n)); - val finite_def = - ("finite_def", - %%:(dname^"_finite") == - mk_lam(x_name, - mk_ex("n",(%%:(dname^"_take") $ Bound 0)`Bound 1 === Bound 1))); - - in (dnam, - [abs_iso_ax, rep_iso_ax, reach_ax], - [when_def, copy_def] @ - con_defs @ dis_defs @ mat_defs @ pat_defs @ sel_defs @ - [take_def, finite_def]) - end; (* let (calc_axioms) *) - - -(* legacy type inference *) - -fun legacy_infer_term thy t = - singleton (Syntax.check_terms (ProofContext.init thy)) (Sign.intern_term thy t); - -fun legacy_infer_prop thy t = legacy_infer_term thy (TypeInfer.constrain propT t); - -fun infer_props thy = map (apsnd (legacy_infer_prop thy)); - - -fun add_axioms_i x = snd o PureThy.add_axioms (map (Thm.no_attributes o apfst Binding.name) x); -fun add_axioms_infer axms thy = add_axioms_i (infer_props thy axms) thy; - -fun add_defs_i x = snd o (PureThy.add_defs false) (map (Thm.no_attributes o apfst Binding.name) x); -fun add_defs_infer defs thy = add_defs_i (infer_props thy defs) thy; - -fun add_matchers (((dname,_),cons) : eq) thy = - let - val con_names = map fst cons; - val mat_names = map mat_name con_names; - fun qualify n = Sign.full_name thy (Binding.name n); - val ms = map qualify con_names ~~ map qualify mat_names; - in Fixrec.add_matchers ms thy end; - -fun add_axioms comp_dnam (eqs : eq list) thy' = - let - val comp_dname = Sign.full_bname thy' comp_dnam; - val dnames = map (fst o fst) eqs; - val x_name = idx_name dnames "x"; - fun copy_app dname = %%:(dname^"_copy")`Bound 0; - val copy_def = ("copy_def" , %%:(comp_dname^"_copy") == - /\ "f"(mk_ctuple (map copy_app dnames))); - - fun one_con (con,args) = let - val nonrec_args = filter_out is_rec args; - val rec_args = List.filter is_rec args; - val recs_cnt = length rec_args; - val allargs = nonrec_args @ rec_args - @ map (upd_vname (fn s=> s^"'")) rec_args; - val allvns = map vname allargs; - fun vname_arg s arg = if is_rec arg then vname arg^s else vname arg; - val vns1 = map (vname_arg "" ) args; - val vns2 = map (vname_arg "'") args; - val allargs_cnt = length nonrec_args + 2*recs_cnt; - val rec_idxs = (recs_cnt-1) downto 0; - val nonlazy_idxs = map snd (filter_out (fn (arg,_) => is_lazy arg) - (allargs~~((allargs_cnt-1) downto 0))); - fun rel_app i ra = proj (Bound(allargs_cnt+2)) eqs (rec_of ra) $ - Bound (2*recs_cnt-i) $ Bound (recs_cnt-i); - val capps = - List.foldr mk_conj - (mk_conj( - Bound(allargs_cnt+1)===list_ccomb(%%:con,map (bound_arg allvns) vns1), - Bound(allargs_cnt+0)===list_ccomb(%%:con,map (bound_arg allvns) vns2))) - (mapn rel_app 1 rec_args); - in List.foldr mk_ex - (Library.foldr mk_conj - (map (defined o Bound) nonlazy_idxs,capps)) allvns - end; - fun one_comp n (_,cons) = - mk_all(x_name(n+1), - mk_all(x_name(n+1)^"'", - mk_imp(proj (Bound 2) eqs n $ Bound 1 $ Bound 0, - foldr1 mk_disj (mk_conj(Bound 1 === UU,Bound 0 === UU) - ::map one_con cons)))); - val bisim_def = - ("bisim_def", - %%:(comp_dname^"_bisim")==mk_lam("R", foldr1 mk_conj (mapn one_comp 0 eqs))); - - fun add_one (thy,(dnam,axs,dfs)) = - thy |> Sign.add_path dnam - |> add_defs_infer dfs - |> add_axioms_infer axs - |> Sign.parent_path; - - val thy = Library.foldl add_one (thy', mapn (calc_axioms comp_dname eqs) 0 eqs); - - in thy |> Sign.add_path comp_dnam - |> add_defs_infer (bisim_def::(if length eqs>1 then [copy_def] else [])) - |> Sign.parent_path - |> fold add_matchers eqs - end; (* let (add_axioms) *) - -end; (* struct *) diff -r 6da9c2a49fed -r 631546213601 src/HOLCF/Tools/domain/domain_extender.ML --- a/src/HOLCF/Tools/domain/domain_extender.ML Tue Jul 21 14:08:58 2009 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,204 +0,0 @@ -(* Title: HOLCF/Tools/domain/domain_extender.ML - Author: David von Oheimb - -Theory extender for domain command, including theory syntax. -*) - -signature DOMAIN_EXTENDER = -sig - val add_domain_cmd: string -> - ((string * string option) list * binding * mixfix * - (binding * (bool * binding option * string) list * mixfix) list) list - -> theory -> theory - val add_domain: string -> - ((string * string option) list * binding * mixfix * - (binding * (bool * binding option * typ) list * mixfix) list) list - -> theory -> theory -end; - -structure Domain_Extender :> DOMAIN_EXTENDER = -struct - -open Domain_Library; - -(* ----- general testing and preprocessing of constructor list -------------- *) -fun check_and_sort_domain - (dtnvs : (string * typ list) list) - (cons'' : (binding * (bool * binding option * typ) list * mixfix) list list) - (sg : theory) - : ((string * typ list) * - (binding * (bool * binding option * typ) list * mixfix) list) list = - let - val defaultS = Sign.defaultS sg; - val test_dupl_typs = (case duplicates (op =) (map fst dtnvs) of - [] => false | dups => error ("Duplicate types: " ^ commas_quote dups)); - val test_dupl_cons = - (case duplicates (op =) (map (Binding.name_of o first) (List.concat cons'')) of - [] => false | dups => error ("Duplicate constructors: " - ^ commas_quote dups)); - val test_dupl_sels = - (case duplicates (op =) (map Binding.name_of (List.mapPartial second - (List.concat (map second (List.concat cons''))))) of - [] => false | dups => error("Duplicate selectors: "^commas_quote dups)); - val test_dupl_tvars = - exists(fn s=>case duplicates (op =) (map(fst o dest_TFree)s)of - [] => false | dups => error("Duplicate type arguments: " - ^commas_quote dups)) (map snd dtnvs); - (* test for free type variables, illegal sort constraints on rhs, - non-pcpo-types and invalid use of recursive type; - replace sorts in type variables on rhs *) - fun analyse_equation ((dname,typevars),cons') = - let - val tvars = map dest_TFree typevars; - val distinct_typevars = map TFree tvars; - fun rm_sorts (TFree(s,_)) = TFree(s,[]) - | rm_sorts (Type(s,ts)) = Type(s,remove_sorts ts) - | rm_sorts (TVar(s,_)) = TVar(s,[]) - and remove_sorts l = map rm_sorts l; - val indirect_ok = ["*","Cfun.->","Ssum.++","Sprod.**","Up.u"] - fun analyse indirect (TFree(v,s)) = - (case AList.lookup (op =) tvars v of - NONE => error ("Free type variable " ^ quote v ^ " on rhs.") - | SOME sort => if eq_set_string (s,defaultS) orelse - eq_set_string (s,sort ) - then TFree(v,sort) - else error ("Inconsistent sort constraint" ^ - " for type variable " ^ quote v)) - | analyse indirect (t as Type(s,typl)) = - (case AList.lookup (op =) dtnvs s of - NONE => if s mem indirect_ok - then Type(s,map (analyse false) typl) - else Type(s,map (analyse true) typl) - | SOME typevars => if indirect - then error ("Indirect recursion of type " ^ - quote (string_of_typ sg t)) - else if dname <> s orelse - (** BUG OR FEATURE?: - mutual recursion may use different arguments **) - remove_sorts typevars = remove_sorts typl - then Type(s,map (analyse true) typl) - else error ("Direct recursion of type " ^ - quote (string_of_typ sg t) ^ - " with different arguments")) - | analyse indirect (TVar _) = Imposs "extender:analyse"; - fun check_pcpo lazy T = - let val ok = if lazy then cpo_type else pcpo_type - in if ok sg T then T else error - ("Constructor argument type is not of sort pcpo: " ^ - string_of_typ sg T) - end; - fun analyse_arg (lazy, sel, T) = - (lazy, sel, check_pcpo lazy (analyse false T)); - fun analyse_con (b, args, mx) = (b, map analyse_arg args, mx); - in ((dname,distinct_typevars), map analyse_con cons') end; - in ListPair.map analyse_equation (dtnvs,cons'') - end; (* let *) - -(* ----- calls for building new thy and thms -------------------------------- *) - -fun gen_add_domain - (prep_typ : theory -> 'a -> typ) - (comp_dnam : string) - (eqs''' : ((string * string option) list * binding * mixfix * - (binding * (bool * binding option * 'a) list * mixfix) list) list) - (thy''' : theory) = - let - fun readS (SOME s) = Syntax.read_sort_global thy''' s - | readS NONE = Sign.defaultS thy'''; - fun readTFree (a, s) = TFree (a, readS s); - - val dtnvs = map (fn (vs,dname:binding,mx,_) => - (dname, map readTFree vs, mx)) eqs'''; - val cons''' = map (fn (_,_,_,cons) => cons) eqs'''; - fun thy_type (dname,tvars,mx) = (dname, length tvars, mx); - fun thy_arity (dname,tvars,mx) = (Sign.full_name thy''' dname, map (snd o dest_TFree) tvars, pcpoS); - val thy'' = thy''' |> Sign.add_types (map thy_type dtnvs) - |> fold (AxClass.axiomatize_arity o thy_arity) dtnvs; - val cons'' = map (map (upd_second (map (upd_third (prep_typ thy''))))) cons'''; - val dtnvs' = map (fn (dname,vs,mx) => (Sign.full_name thy''' dname,vs)) dtnvs; - val eqs' : ((string * typ list) * (binding * (bool * binding option * typ) list * mixfix) list) list = - check_and_sort_domain dtnvs' cons'' thy''; - val thy' = thy'' |> Domain_Syntax.add_syntax comp_dnam eqs'; - val dts = map (Type o fst) eqs'; - val new_dts = map (fn ((s,Ts),_) => (s, map (fst o dest_TFree) Ts)) eqs'; - fun strip ss = Library.drop (find_index (fn s => s = "'") ss + 1, ss); - fun typid (Type (id,_)) = - let val c = hd (Symbol.explode (Long_Name.base_name id)) - in if Symbol.is_letter c then c else "t" end - | typid (TFree (id,_) ) = hd (strip (tl (Symbol.explode id))) - | typid (TVar ((id,_),_)) = hd (tl (Symbol.explode id)); - fun one_con (con,args,mx) = - ((Syntax.const_name mx (Binding.name_of con)), - ListPair.map (fn ((lazy,sel,tp),vn) => mk_arg ((lazy, - DatatypeAux.dtyp_of_typ new_dts tp), - Option.map Binding.name_of sel,vn)) - (args,(mk_var_names(map (typid o third) args))) - ) : cons; - val eqs = map (fn (dtnvs,cons') => (dtnvs, map one_con cons')) eqs' : eq list; - val thy = thy' |> Domain_Axioms.add_axioms comp_dnam eqs; - val ((rewss, take_rews), theorems_thy) = - thy |> fold_map (fn eq => Domain_Theorems.theorems (eq, eqs)) eqs - ||>> Domain_Theorems.comp_theorems (comp_dnam, eqs); - in - theorems_thy - |> Sign.add_path (Long_Name.base_name comp_dnam) - |> (snd o (PureThy.add_thmss [((Binding.name "rews", List.concat rewss @ take_rews), [])])) - |> Sign.parent_path - end; - -val add_domain = gen_add_domain Sign.certify_typ; -val add_domain_cmd = gen_add_domain Syntax.read_typ_global; - - -(** outer syntax **) - -local structure P = OuterParse and K = OuterKeyword in - -val _ = OuterKeyword.keyword "lazy"; - -val dest_decl : (bool * binding option * string) parser = - P.$$$ "(" |-- Scan.optional (P.$$$ "lazy" >> K true) false -- - (P.binding >> SOME) -- (P.$$$ "::" |-- P.typ) --| P.$$$ ")" >> P.triple1 - || P.$$$ "(" |-- P.$$$ "lazy" |-- P.typ --| P.$$$ ")" - >> (fn t => (true,NONE,t)) - || P.typ >> (fn t => (false,NONE,t)); - -val cons_decl = - P.binding -- Scan.repeat dest_decl -- P.opt_mixfix; - -val type_var' : (string * string option) parser = - (P.type_ident -- Scan.option (P.$$$ "::" |-- P.!!! P.sort)); - -val type_args' : (string * string option) list parser = - type_var' >> single || - P.$$$ "(" |-- P.!!! (P.list1 type_var' --| P.$$$ ")") || - Scan.succeed []; - -val domain_decl = - (type_args' -- P.binding -- P.opt_infix) -- - (P.$$$ "=" |-- P.enum1 "|" cons_decl); - -val domains_decl = - Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") -- - P.and_list1 domain_decl; - -fun mk_domain (opt_name : string option, - doms : ((((string * string option) list * binding) * mixfix) * - ((binding * (bool * binding option * string) list) * mixfix) list) list ) = - let - val names = map (fn (((_, t), _), _) => Binding.name_of t) doms; - val specs : ((string * string option) list * binding * mixfix * - (binding * (bool * binding option * string) list * mixfix) list) list = - map (fn (((vs, t), mx), cons) => - (vs, t, mx, map (fn ((c, ds), mx) => (c, ds, mx)) cons)) doms; - val comp_dnam = - case opt_name of NONE => space_implode "_" names | SOME s => s; - in add_domain_cmd comp_dnam specs end; - -val _ = - OuterSyntax.command "domain" "define recursive domains (HOLCF)" K.thy_decl - (domains_decl >> (Toplevel.theory o mk_domain)); - -end; - -end; diff -r 6da9c2a49fed -r 631546213601 src/HOLCF/Tools/domain/domain_library.ML --- a/src/HOLCF/Tools/domain/domain_library.ML Tue Jul 21 14:08:58 2009 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,399 +0,0 @@ -(* Title: HOLCF/Tools/domain/domain_library.ML - Author: David von Oheimb - -Library for domain command. -*) - - -(* ----- general support ---------------------------------------------------- *) - -fun mapn f n [] = [] - | mapn f n (x::xs) = (f n x) :: mapn f (n+1) xs; - -fun foldr'' f (l,f2) = - let fun itr [] = raise Fail "foldr''" - | itr [a] = f2 a - | itr (a::l) = f(a, itr l) - in itr l end; - -fun map_cumulr f start xs = - List.foldr (fn (x,(ys,res))=>case f(x,res) of (y,res2) => - (y::ys,res2)) ([],start) xs; - -fun first (x,_,_) = x; fun second (_,x,_) = x; fun third (_,_,x) = x; -fun upd_first f (x,y,z) = (f x, y, z); -fun upd_second f (x,y,z) = ( x, f y, z); -fun upd_third f (x,y,z) = ( x, y, f z); - -fun atomize ctxt thm = - let - val r_inst = read_instantiate ctxt; - fun at thm = - case concl_of thm of - _$(Const("op &",_)$_$_) => at(thm RS conjunct1)@at(thm RS conjunct2) - | _$(Const("All" ,_)$Abs(s,_,_))=> at(thm RS (r_inst [(("x", 0), "?" ^ s)] spec)) - | _ => [thm]; - in map zero_var_indexes (at thm) end; - -(* infix syntax *) - -infixr 5 -->; -infixr 6 ->>; -infixr 0 ===>; -infixr 0 ==>; -infix 0 ==; -infix 1 ===; -infix 1 ~=; -infix 1 <<; -infix 1 ~<<; - -infix 9 ` ; -infix 9 `% ; -infix 9 `%%; - - -(* ----- specific support for domain ---------------------------------------- *) - -signature DOMAIN_LIBRARY = -sig - val Imposs : string -> 'a; - val cpo_type : theory -> typ -> bool; - val pcpo_type : theory -> typ -> bool; - val string_of_typ : theory -> typ -> string; - - (* Creating HOLCF types *) - val mk_cfunT : typ * typ -> typ; - val ->> : typ * typ -> typ; - val mk_ssumT : typ * typ -> typ; - val mk_sprodT : typ * typ -> typ; - val mk_uT : typ -> typ; - val oneT : typ; - val trT : typ; - val mk_maybeT : typ -> typ; - val mk_ctupleT : typ list -> typ; - val mk_TFree : string -> typ; - val pcpoS : sort; - - (* Creating HOLCF terms *) - val %: : string -> term; - val %%: : string -> term; - val ` : term * term -> term; - val `% : term * string -> term; - val /\ : string -> term -> term; - val UU : term; - val TT : term; - val FF : term; - val ID : term; - val oo : term * term -> term; - val mk_up : term -> term; - val mk_sinl : term -> term; - val mk_sinr : term -> term; - val mk_stuple : term list -> term; - val mk_ctuple : term list -> term; - val mk_fix : term -> term; - val mk_iterate : term * term * term -> term; - val mk_fail : term; - val mk_return : term -> term; - val cproj : term -> 'a list -> int -> term; - val list_ccomb : term * term list -> term; - (* - val con_app : string -> ('a * 'b * string) list -> term; - *) - val con_app2 : string -> ('a -> term) -> 'a list -> term; - val proj : term -> 'a list -> int -> term; - val prj : ('a -> 'b -> 'a) -> ('a -> 'b -> 'a) -> 'a -> 'b list -> int -> 'a; - val mk_ctuple_pat : term list -> term; - val mk_branch : term -> term; - - (* Creating propositions *) - val mk_conj : term * term -> term; - val mk_disj : term * term -> term; - val mk_imp : term * term -> term; - val mk_lam : string * term -> term; - val mk_all : string * term -> term; - val mk_ex : string * term -> term; - val mk_constrain : typ * term -> term; - val mk_constrainall : string * typ * term -> term; - val === : term * term -> term; - val << : term * term -> term; - val ~<< : term * term -> term; - val strict : term -> term; - val defined : term -> term; - val mk_adm : term -> term; - val mk_compact : term -> term; - val lift : ('a -> term) -> 'a list * term -> term; - val lift_defined : ('a -> term) -> 'a list * term -> term; - - (* Creating meta-propositions *) - val mk_trp : term -> term; (* HOLogic.mk_Trueprop *) - val == : term * term -> term; - val ===> : term * term -> term; - val ==> : term * term -> term; - val mk_All : string * term -> term; - - (* Domain specifications *) - eqtype arg; - type cons = string * arg list; - type eq = (string * typ list) * cons list; - val mk_arg : (bool * Datatype.dtyp) * string option * string -> arg; - val is_lazy : arg -> bool; - val rec_of : arg -> int; - val dtyp_of : arg -> Datatype.dtyp; - val sel_of : arg -> string option; - val vname : arg -> string; - val upd_vname : (string -> string) -> arg -> arg; - val is_rec : arg -> bool; - val is_nonlazy_rec : arg -> bool; - val nonlazy : arg list -> string list; - val nonlazy_rec : arg list -> string list; - val %# : arg -> term; - val /\# : arg * term -> term; - val when_body : cons list -> (int * int -> term) -> term; - val when_funs : 'a list -> string list; - val bound_arg : ''a list -> ''a -> term; (* ''a = arg or string *) - val idx_name : 'a list -> string -> int -> string; - val app_rec_arg : (int -> term) -> arg -> term; - val con_app : string -> arg list -> term; - val dtyp_of_eq : eq -> Datatype.dtyp; - - - (* Name mangling *) - val strip_esc : string -> string; - val extern_name : string -> string; - val dis_name : string -> string; - val mat_name : string -> string; - val pat_name : string -> string; - val mk_var_names : string list -> string list; -end; - -structure Domain_Library :> DOMAIN_LIBRARY = -struct - -exception Impossible of string; -fun Imposs msg = raise Impossible ("Domain:"^msg); - -(* ----- name handling ----- *) - -val strip_esc = - let fun strip ("'" :: c :: cs) = c :: strip cs - | strip ["'"] = [] - | strip (c :: cs) = c :: strip cs - | strip [] = []; - in implode o strip o Symbol.explode end; - -fun extern_name con = - case Symbol.explode con of - ("o"::"p"::" "::rest) => implode rest - | _ => con; -fun dis_name con = "is_"^ (extern_name con); -fun dis_name_ con = "is_"^ (strip_esc con); -fun mat_name con = "match_"^ (extern_name con); -fun mat_name_ con = "match_"^ (strip_esc con); -fun pat_name con = (extern_name con) ^ "_pat"; -fun pat_name_ con = (strip_esc con) ^ "_pat"; - -(* make distinct names out of the type list, - forbidding "o","n..","x..","f..","P.." as names *) -(* a number string is added if necessary *) -fun mk_var_names ids : string list = - let - fun nonreserved s = if s mem ["n","x","f","P"] then s^"'" else s; - fun index_vnames(vn::vns,occupied) = - (case AList.lookup (op =) occupied vn of - NONE => if vn mem vns - then (vn^"1") :: index_vnames(vns,(vn,1) ::occupied) - else vn :: index_vnames(vns, occupied) - | SOME(i) => (vn^(string_of_int (i+1))) - :: index_vnames(vns,(vn,i+1)::occupied)) - | index_vnames([],occupied) = []; - in index_vnames(map nonreserved ids, [("O",0),("o",0)]) end; - -fun cpo_type sg t = Sign.of_sort sg (Sign.certify_typ sg t, @{sort cpo}); -fun pcpo_type sg t = Sign.of_sort sg (Sign.certify_typ sg t, @{sort pcpo}); -fun string_of_typ sg = Syntax.string_of_typ_global sg o Sign.certify_typ sg; - -(* ----- constructor list handling ----- *) - -type arg = - (bool * Datatype.dtyp) * (* (lazy, recursive element) *) - string option * (* selector name *) - string; (* argument name *) - -type cons = - string * (* operator name of constr *) - arg list; (* argument list *) - -type eq = - (string * (* name of abstracted type *) - typ list) * (* arguments of abstracted type *) - cons list; (* represented type, as a constructor list *) - -val mk_arg = I; - -fun rec_of ((_,dtyp),_,_) = - case dtyp of DatatypeAux.DtRec i => i | _ => ~1; -(* FIXME: what about indirect recursion? *) - -fun is_lazy arg = fst (first arg); -fun dtyp_of arg = snd (first arg); -val sel_of = second; -val vname = third; -val upd_vname = upd_third; -fun is_rec arg = rec_of arg >=0; -fun is_nonlazy_rec arg = is_rec arg andalso not (is_lazy arg); -fun nonlazy args = map vname (filter_out is_lazy args); -fun nonlazy_rec args = map vname (List.filter is_nonlazy_rec args); - - -(* ----- combinators for making dtyps ----- *) - -fun mk_uD T = DatatypeAux.DtType(@{type_name "u"}, [T]); -fun mk_sprodD (T, U) = DatatypeAux.DtType(@{type_name "**"}, [T, U]); -fun mk_ssumD (T, U) = DatatypeAux.DtType(@{type_name "++"}, [T, U]); -fun mk_liftD T = DatatypeAux.DtType(@{type_name "lift"}, [T]); -val unitD = DatatypeAux.DtType(@{type_name "unit"}, []); -val boolD = DatatypeAux.DtType(@{type_name "bool"}, []); -val oneD = mk_liftD unitD; -val trD = mk_liftD boolD; -fun big_sprodD ds = case ds of [] => oneD | _ => foldr1 mk_sprodD ds; -fun big_ssumD ds = case ds of [] => unitD | _ => foldr1 mk_ssumD ds; - -fun dtyp_of_arg ((lazy, D), _, _) = if lazy then mk_uD D else D; -fun dtyp_of_cons (_, args) = big_sprodD (map dtyp_of_arg args); -fun dtyp_of_eq (_, cons) = big_ssumD (map dtyp_of_cons cons); - - -(* ----- support for type and mixfix expressions ----- *) - -fun mk_uT T = Type(@{type_name "u"}, [T]); -fun mk_cfunT (T, U) = Type(@{type_name "->"}, [T, U]); -fun mk_sprodT (T, U) = Type(@{type_name "**"}, [T, U]); -fun mk_ssumT (T, U) = Type(@{type_name "++"}, [T, U]); -val oneT = @{typ one}; -val trT = @{typ tr}; - -val op ->> = mk_cfunT; - -fun mk_TFree s = TFree ("'" ^ s, @{sort pcpo}); - -(* ----- support for term expressions ----- *) - -fun %: s = Free(s,dummyT); -fun %# arg = %:(vname arg); -fun %%: s = Const(s,dummyT); - -local open HOLogic in -val mk_trp = mk_Trueprop; -fun mk_conj (S,T) = conj $ S $ T; -fun mk_disj (S,T) = disj $ S $ T; -fun mk_imp (S,T) = imp $ S $ T; -fun mk_lam (x,T) = Abs(x,dummyT,T); -fun mk_all (x,P) = HOLogic.mk_all (x,dummyT,P); -fun mk_ex (x,P) = mk_exists (x,dummyT,P); -val mk_constrain = uncurry TypeInfer.constrain; -fun mk_constrainall (x,typ,P) = %%:"All" $ (TypeInfer.constrain (typ --> boolT) (mk_lam(x,P))); -end - -fun mk_All (x,P) = %%:"all" $ mk_lam(x,P); (* meta universal quantification *) - -infixr 0 ===>; fun S ===> T = %%:"==>" $ S $ T; -infixr 0 ==>; fun S ==> T = mk_trp S ===> mk_trp T; -infix 0 ==; fun S == T = %%:"==" $ S $ T; -infix 1 ===; fun S === T = %%:"op =" $ S $ T; -infix 1 ~=; fun S ~= T = HOLogic.mk_not (S === T); -infix 1 <<; fun S << T = %%: @{const_name Porder.below} $ S $ T; -infix 1 ~<<; fun S ~<< T = HOLogic.mk_not (S << T); - -infix 9 ` ; fun f ` x = %%: @{const_name Rep_CFun} $ f $ x; -infix 9 `% ; fun f`% s = f` %: s; -infix 9 `%%; fun f`%%s = f` %%:s; - -fun mk_adm t = %%: @{const_name adm} $ t; -fun mk_compact t = %%: @{const_name compact} $ t; -val ID = %%: @{const_name ID}; -fun mk_strictify t = %%: @{const_name strictify}`t; -fun mk_cfst t = %%: @{const_name cfst}`t; -fun mk_csnd t = %%: @{const_name csnd}`t; -(*val csplitN = "Cprod.csplit";*) -(*val sfstN = "Sprod.sfst";*) -(*val ssndN = "Sprod.ssnd";*) -fun mk_ssplit t = %%: @{const_name ssplit}`t; -fun mk_sinl t = %%: @{const_name sinl}`t; -fun mk_sinr t = %%: @{const_name sinr}`t; -fun mk_sscase (x, y) = %%: @{const_name sscase}`x`y; -fun mk_up t = %%: @{const_name up}`t; -fun mk_fup (t,u) = %%: @{const_name fup} ` t ` u; -val ONE = @{term ONE}; -val TT = @{term TT}; -val FF = @{term FF}; -fun mk_iterate (n,f,z) = %%: @{const_name iterate} $ n ` f ` z; -fun mk_fix t = %%: @{const_name fix}`t; -fun mk_return t = %%: @{const_name Fixrec.return}`t; -val mk_fail = %%: @{const_name Fixrec.fail}; - -fun mk_branch t = %%: @{const_name Fixrec.branch} $ t; - -val pcpoS = @{sort pcpo}; - -val list_ccomb = Library.foldl (op `); (* continuous version of list_comb *) -fun con_app2 con f args = list_ccomb(%%:con,map f args); -fun con_app con = con_app2 con %#; -fun if_rec arg f y = if is_rec arg then f (rec_of arg) else y; -fun app_rec_arg p arg = if_rec arg (fn n => fn x => (p n)`x) I (%# arg); -fun prj _ _ x ( _::[]) _ = x - | prj f1 _ x (_::y::ys) 0 = f1 x y - | prj f1 f2 x (y:: ys) j = prj f1 f2 (f2 x y) ys (j-1); -fun proj x = prj (fn S => K(%%:"fst" $S)) (fn S => K(%%:"snd" $S)) x; -fun cproj x = prj (fn S => K(mk_cfst S)) (fn S => K(mk_csnd S)) x; -fun lift tfn = Library.foldr (fn (x,t)=> (mk_trp(tfn x) ===> t)); - -fun /\ v T = %%: @{const_name Abs_CFun} $ mk_lam(v,T); -fun /\# (arg,T) = /\ (vname arg) T; -infixr 9 oo; fun S oo T = %%: @{const_name cfcomp}`S`T; -val UU = %%: @{const_name UU}; -fun strict f = f`UU === UU; -fun defined t = t ~= UU; -fun cpair (t,u) = %%: @{const_name cpair}`t`u; -fun spair (t,u) = %%: @{const_name spair}`t`u; -fun mk_ctuple [] = HOLogic.unit (* used in match_defs *) - | mk_ctuple ts = foldr1 cpair ts; -fun mk_stuple [] = ONE - | mk_stuple ts = foldr1 spair ts; -fun mk_ctupleT [] = HOLogic.unitT (* used in match_defs *) - | mk_ctupleT Ts = foldr1 HOLogic.mk_prodT Ts; -fun mk_maybeT T = Type ("Fixrec.maybe",[T]); -fun cpair_pat (p1,p2) = %%: @{const_name cpair_pat} $ p1 $ p2; -val mk_ctuple_pat = foldr1 cpair_pat; -fun lift_defined f = lift (fn x => defined (f x)); -fun bound_arg vns v = Bound (length vns - find_index (fn v' => v' = v) vns - 1); - -fun cont_eta_contract (Const("Cfun.Abs_CFun",TT) $ Abs(a,T,body)) = - (case cont_eta_contract body of - body' as (Const("Cfun.Rep_CFun",Ta) $ f $ Bound 0) => - if not (0 mem loose_bnos f) then incr_boundvars ~1 f - else Const("Cfun.Abs_CFun",TT) $ Abs(a,T,body') - | body' => Const("Cfun.Abs_CFun",TT) $ Abs(a,T,body')) - | cont_eta_contract(f$t) = cont_eta_contract f $ cont_eta_contract t - | cont_eta_contract t = t; - -fun idx_name dnames s n = s^(if length dnames = 1 then "" else string_of_int n); -fun when_funs cons = if length cons = 1 then ["f"] - else mapn (fn n => K("f"^(string_of_int n))) 1 cons; -fun when_body cons funarg = - let - fun one_fun n (_,[] ) = /\ "dummy" (funarg(1,n)) - | one_fun n (_,args) = let - val l2 = length args; - fun idxs m arg = (if is_lazy arg then (fn t => mk_fup (ID, t)) - else I) (Bound(l2-m)); - in cont_eta_contract - (foldr'' - (fn (a,t) => mk_ssplit (/\# (a,t))) - (args, - fn a=> /\#(a,(list_ccomb(funarg(l2,n),mapn idxs 1 args)))) - ) end; - in (if length cons = 1 andalso length(snd(hd cons)) <= 1 - then mk_strictify else I) - (foldr1 mk_sscase (mapn one_fun 1 cons)) end; - -end; (* struct *) diff -r 6da9c2a49fed -r 631546213601 src/HOLCF/Tools/domain/domain_syntax.ML --- a/src/HOLCF/Tools/domain/domain_syntax.ML Tue Jul 21 14:08:58 2009 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,181 +0,0 @@ -(* Title: HOLCF/Tools/domain/domain_syntax.ML - Author: David von Oheimb - -Syntax generator for domain command. -*) - -signature DOMAIN_SYNTAX = -sig - val calc_syntax: - typ -> - (string * typ list) * - (binding * (bool * binding option * typ) list * mixfix) list -> - (binding * typ * mixfix) list * ast Syntax.trrule list - - val add_syntax: - string -> - ((string * typ list) * - (binding * (bool * binding option * typ) list * mixfix) list) list -> - theory -> theory -end; - - -structure Domain_Syntax :> DOMAIN_SYNTAX = -struct - -open Domain_Library; -infixr 5 -->; infixr 6 ->>; - -fun calc_syntax - (dtypeprod : typ) - ((dname : string, typevars : typ list), - (cons': (binding * (bool * binding option * typ) list * mixfix) list)) - : (binding * typ * mixfix) list * ast Syntax.trrule list = - let - (* ----- constants concerning the isomorphism ------------------------------- *) - - local - fun opt_lazy (lazy,_,t) = if lazy then mk_uT t else t - fun prod (_,args,_) = case args of [] => oneT - | _ => foldr1 mk_sprodT (map opt_lazy args); - fun freetvar s = let val tvar = mk_TFree s in - if tvar mem typevars then freetvar ("t"^s) else tvar end; - fun when_type (_,args,_) = List.foldr (op ->>) (freetvar "t") (map third args); - in - val dtype = Type(dname,typevars); - val dtype2 = foldr1 mk_ssumT (map prod cons'); - val dnam = Long_Name.base_name dname; - fun dbind s = Binding.name (dnam ^ s); - val const_rep = (dbind "_rep" , dtype ->> dtype2, NoSyn); - val const_abs = (dbind "_abs" , dtype2 ->> dtype , NoSyn); - val const_when = (dbind "_when", List.foldr (op ->>) (dtype ->> freetvar "t") (map when_type cons'), NoSyn); - val const_copy = (dbind "_copy", dtypeprod ->> dtype ->> dtype , NoSyn); - end; - - (* ----- constants concerning constructors, discriminators, and selectors --- *) - - local - val escape = let - fun esc (c::cs) = if c mem ["'","_","(",")","/"] then "'"::c::esc cs - else c::esc cs - | esc [] = [] - in implode o esc o Symbol.explode end; - fun dis_name_ con = Binding.name ("is_" ^ strip_esc (Binding.name_of con)); - fun mat_name_ con = Binding.name ("match_" ^ strip_esc (Binding.name_of con)); - fun pat_name_ con = Binding.name (strip_esc (Binding.name_of con) ^ "_pat"); - fun con (name,args,mx) = (name, List.foldr (op ->>) dtype (map third args), mx); - fun dis (con,args,mx) = (dis_name_ con, dtype->>trT, - Mixfix(escape ("is_" ^ Binding.name_of con), [], Syntax.max_pri)); - (* strictly speaking, these constants have one argument, - but the mixfix (without arguments) is introduced only - to generate parse rules for non-alphanumeric names*) - fun freetvar s n = let val tvar = mk_TFree (s ^ string_of_int n) in - if tvar mem typevars then freetvar ("t"^s) n else tvar end; - fun mk_matT (a,bs,c) = a ->> foldr (op ->>) (mk_maybeT c) bs ->> mk_maybeT c; - fun mat (con,args,mx) = (mat_name_ con, - mk_matT(dtype, map third args, freetvar "t" 1), - Mixfix(escape ("match_" ^ Binding.name_of con), [], Syntax.max_pri)); - fun sel1 (_,sel,typ) = Option.map (fn s => (s,dtype ->> typ,NoSyn)) sel; - fun sel (con,args,mx) = List.mapPartial sel1 args; - fun mk_patT (a,b) = a ->> mk_maybeT b; - fun pat_arg_typ n arg = mk_patT (third arg, freetvar "t" n); - fun pat (con,args,mx) = (pat_name_ con, - (mapn pat_arg_typ 1 args) - ---> - mk_patT (dtype, mk_ctupleT (map (freetvar "t") (1 upto length args))), - Mixfix(escape (Binding.name_of con ^ "_pat"), [], Syntax.max_pri)); - - in - val consts_con = map con cons'; - val consts_dis = map dis cons'; - val consts_mat = map mat cons'; - val consts_pat = map pat cons'; - val consts_sel = List.concat(map sel cons'); - end; - - (* ----- constants concerning induction ------------------------------------- *) - - val const_take = (dbind "_take" , HOLogic.natT-->dtype->>dtype, NoSyn); - val const_finite = (dbind "_finite", dtype-->HOLogic.boolT , NoSyn); - - (* ----- case translation --------------------------------------------------- *) - - local open Syntax in - local - fun c_ast con mx = Constant (Syntax.const_name mx (Binding.name_of con)); - fun expvar n = Variable ("e"^(string_of_int n)); - fun argvar n m _ = Variable ("a"^(string_of_int n)^"_"^ - (string_of_int m)); - fun argvars n args = mapn (argvar n) 1 args; - fun app s (l,r) = mk_appl (Constant s) [l,r]; - val cabs = app "_cabs"; - val capp = app "Rep_CFun"; - fun con1 n (con,args,mx) = Library.foldl capp (c_ast con mx, argvars n args); - fun case1 n (con,args,mx) = app "_case1" (con1 n (con,args,mx), expvar n); - fun arg1 n (con,args,_) = List.foldr cabs (expvar n) (argvars n args); - fun when1 n m = if n = m then arg1 n else K (Constant "UU"); - - fun app_var x = mk_appl (Constant "_variable") [x, Variable "rhs"]; - fun app_pat x = mk_appl (Constant "_pat") [x]; - fun args_list [] = Constant "_noargs" - | args_list xs = foldr1 (app "_args") xs; - in - val case_trans = - ParsePrintRule - (app "_case_syntax" (Variable "x", foldr1 (app "_case2") (mapn case1 1 cons')), - capp (Library.foldl capp (Constant (dnam^"_when"), mapn arg1 1 cons'), Variable "x")); - - fun one_abscon_trans n (con,mx,args) = - ParsePrintRule - (cabs (con1 n (con,mx,args), expvar n), - Library.foldl capp (Constant (dnam^"_when"), mapn (when1 n) 1 cons')); - val abscon_trans = mapn one_abscon_trans 1 cons'; - - fun one_case_trans (con,args,mx) = - let - val cname = c_ast con mx; - val pname = Constant (strip_esc (Binding.name_of con) ^ "_pat"); - val ns = 1 upto length args; - val xs = map (fn n => Variable ("x"^(string_of_int n))) ns; - val ps = map (fn n => Variable ("p"^(string_of_int n))) ns; - val vs = map (fn n => Variable ("v"^(string_of_int n))) ns; - in - [ParseRule (app_pat (Library.foldl capp (cname, xs)), - mk_appl pname (map app_pat xs)), - ParseRule (app_var (Library.foldl capp (cname, xs)), - app_var (args_list xs)), - PrintRule (Library.foldl capp (cname, ListPair.map (app "_match") (ps,vs)), - app "_match" (mk_appl pname ps, args_list vs))] - end; - val Case_trans = List.concat (map one_case_trans cons'); - end; - end; - - in ([const_rep, const_abs, const_when, const_copy] @ - consts_con @ consts_dis @ consts_mat @ consts_pat @ consts_sel @ - [const_take, const_finite], - (case_trans::(abscon_trans @ Case_trans))) - end; (* let *) - -(* ----- putting all the syntax stuff together ------------------------------ *) - -fun add_syntax - (comp_dnam : string) - (eqs' : ((string * typ list) * - (binding * (bool * binding option * typ) list * mixfix) list) list) - (thy'' : theory) = - let - val dtypes = map (Type o fst) eqs'; - val boolT = HOLogic.boolT; - val funprod = foldr1 HOLogic.mk_prodT (map (fn tp => tp ->> tp ) dtypes); - val relprod = foldr1 HOLogic.mk_prodT (map (fn tp => tp --> tp --> boolT) dtypes); - val const_copy = (Binding.name (comp_dnam^"_copy"), funprod ->> funprod, NoSyn); - val const_bisim = (Binding.name (comp_dnam^"_bisim"), relprod --> boolT, NoSyn); - val ctt : ((binding * typ * mixfix) list * ast Syntax.trrule list) list = map (calc_syntax funprod) eqs'; - in thy'' |> ContConsts.add_consts_i (List.concat (map fst ctt) @ - (if length eqs'>1 then [const_copy] else[])@ - [const_bisim]) - |> Sign.add_trrules_i (List.concat(map snd ctt)) - end; (* let *) - -end; (* struct *) diff -r 6da9c2a49fed -r 631546213601 src/HOLCF/Tools/domain/domain_theorems.ML --- a/src/HOLCF/Tools/domain/domain_theorems.ML Tue Jul 21 14:08:58 2009 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,1054 +0,0 @@ -(* Title: HOLCF/Tools/domain/domain_theorems.ML - ID: $Id$ - Author: David von Oheimb - New proofs/tactics by Brian Huffman - -Proof generator for domain command. -*) - -val HOLCF_ss = @{simpset}; - -signature DOMAIN_THEOREMS = -sig - val theorems: Domain_Library.eq * Domain_Library.eq list -> theory -> thm list * theory; - val comp_theorems: bstring * Domain_Library.eq list -> theory -> thm list * theory; - val quiet_mode: bool ref; - val trace_domain: bool ref; -end; - -structure Domain_Theorems :> DOMAIN_THEOREMS = -struct - -val quiet_mode = ref false; -val trace_domain = ref false; - -fun message s = if !quiet_mode then () else writeln s; -fun trace s = if !trace_domain then tracing s else (); - -local - -val adm_impl_admw = @{thm adm_impl_admw}; -val adm_all = @{thm adm_all}; -val adm_conj = @{thm adm_conj}; -val adm_subst = @{thm adm_subst}; -val antisym_less_inverse = @{thm below_antisym_inverse}; -val beta_cfun = @{thm beta_cfun}; -val cfun_arg_cong = @{thm cfun_arg_cong}; -val ch2ch_Rep_CFunL = @{thm ch2ch_Rep_CFunL}; -val ch2ch_Rep_CFunR = @{thm ch2ch_Rep_CFunR}; -val chain_iterate = @{thm chain_iterate}; -val compact_ONE = @{thm compact_ONE}; -val compact_sinl = @{thm compact_sinl}; -val compact_sinr = @{thm compact_sinr}; -val compact_spair = @{thm compact_spair}; -val compact_up = @{thm compact_up}; -val contlub_cfun_arg = @{thm contlub_cfun_arg}; -val contlub_cfun_fun = @{thm contlub_cfun_fun}; -val fix_def2 = @{thm fix_def2}; -val injection_eq = @{thm injection_eq}; -val injection_less = @{thm injection_below}; -val lub_equal = @{thm lub_equal}; -val monofun_cfun_arg = @{thm monofun_cfun_arg}; -val retraction_strict = @{thm retraction_strict}; -val spair_eq = @{thm spair_eq}; -val spair_less = @{thm spair_below}; -val sscase1 = @{thm sscase1}; -val ssplit1 = @{thm ssplit1}; -val strictify1 = @{thm strictify1}; -val wfix_ind = @{thm wfix_ind}; - -val iso_intro = @{thm iso.intro}; -val iso_abs_iso = @{thm iso.abs_iso}; -val iso_rep_iso = @{thm iso.rep_iso}; -val iso_abs_strict = @{thm iso.abs_strict}; -val iso_rep_strict = @{thm iso.rep_strict}; -val iso_abs_defin' = @{thm iso.abs_defin'}; -val iso_rep_defin' = @{thm iso.rep_defin'}; -val iso_abs_defined = @{thm iso.abs_defined}; -val iso_rep_defined = @{thm iso.rep_defined}; -val iso_compact_abs = @{thm iso.compact_abs}; -val iso_compact_rep = @{thm iso.compact_rep}; -val iso_iso_swap = @{thm iso.iso_swap}; - -val exh_start = @{thm exh_start}; -val ex_defined_iffs = @{thms ex_defined_iffs}; -val exh_casedist0 = @{thm exh_casedist0}; -val exh_casedists = @{thms exh_casedists}; - -open Domain_Library; -infixr 0 ===>; -infixr 0 ==>; -infix 0 == ; -infix 1 ===; -infix 1 ~= ; -infix 1 <<; -infix 1 ~<<; -infix 9 ` ; -infix 9 `% ; -infix 9 `%%; -infixr 9 oo; - -(* ----- general proof facilities ------------------------------------------- *) - -fun legacy_infer_term thy t = - let val ctxt = ProofContext.set_mode ProofContext.mode_schematic (ProofContext.init thy) - in singleton (Syntax.check_terms ctxt) (Sign.intern_term thy t) end; - -fun pg'' thy defs t tacs = - let - val t' = legacy_infer_term thy t; - val asms = Logic.strip_imp_prems t'; - val prop = Logic.strip_imp_concl t'; - fun tac {prems, context} = - rewrite_goals_tac defs THEN - EVERY (tacs {prems = map (rewrite_rule defs) prems, context = context}) - in Goal.prove_global thy [] asms prop tac end; - -fun pg' thy defs t tacsf = - let - fun tacs {prems, context} = - if null prems then tacsf context - else cut_facts_tac prems 1 :: tacsf context; - in pg'' thy defs t tacs end; - -fun case_UU_tac ctxt rews i v = - InductTacs.case_tac ctxt (v^"=UU") i THEN - asm_simp_tac (HOLCF_ss addsimps rews) i; - -val chain_tac = - REPEAT_DETERM o resolve_tac - [chain_iterate, ch2ch_Rep_CFunR, ch2ch_Rep_CFunL]; - -(* ----- general proofs ----------------------------------------------------- *) - -val all2E = @{lemma "!x y . P x y ==> (P x y ==> R) ==> R" by simp} - -val dist_eqI = @{lemma "!!x::'a::po. ~ x << y ==> x ~= y" by (blast dest!: below_antisym_inverse)} - -in - -fun theorems (((dname, _), cons) : eq, eqs : eq list) thy = -let - -val _ = message ("Proving isomorphism properties of domain "^dname^" ..."); -val pg = pg' thy; - -(* ----- getting the axioms and definitions --------------------------------- *) - -local - fun ga s dn = PureThy.get_thm thy (dn ^ "." ^ s); -in - val ax_abs_iso = ga "abs_iso" dname; - val ax_rep_iso = ga "rep_iso" dname; - val ax_when_def = ga "when_def" dname; - fun get_def mk_name (con,_) = ga (mk_name con^"_def") dname; - val axs_con_def = map (get_def extern_name) cons; - val axs_dis_def = map (get_def dis_name) cons; - val axs_mat_def = map (get_def mat_name) cons; - val axs_pat_def = map (get_def pat_name) cons; - val axs_sel_def = - let - fun def_of_sel sel = ga (sel^"_def") dname; - fun def_of_arg arg = Option.map def_of_sel (sel_of arg); - fun defs_of_con (_, args) = List.mapPartial def_of_arg args; - in - maps defs_of_con cons - end; - val ax_copy_def = ga "copy_def" dname; -end; (* local *) - -(* ----- theorems concerning the isomorphism -------------------------------- *) - -val dc_abs = %%:(dname^"_abs"); -val dc_rep = %%:(dname^"_rep"); -val dc_copy = %%:(dname^"_copy"); -val x_name = "x"; - -val iso_locale = iso_intro OF [ax_abs_iso, ax_rep_iso]; -val abs_strict = ax_rep_iso RS (allI RS retraction_strict); -val rep_strict = ax_abs_iso RS (allI RS retraction_strict); -val abs_defin' = iso_locale RS iso_abs_defin'; -val rep_defin' = iso_locale RS iso_rep_defin'; -val iso_rews = map standard [ax_abs_iso,ax_rep_iso,abs_strict,rep_strict]; - -(* ----- generating beta reduction rules from definitions-------------------- *) - -val _ = trace " Proving beta reduction rules..."; - -local - fun arglist (Const _ $ Abs (s, _, t)) = - let - val (vars,body) = arglist t; - in (s :: vars, body) end - | arglist t = ([], t); - fun bind_fun vars t = Library.foldr mk_All (vars, t); - fun bound_vars 0 = [] - | bound_vars i = Bound (i-1) :: bound_vars (i - 1); -in - fun appl_of_def def = - let - val (_ $ con $ lam) = concl_of def; - val (vars, rhs) = arglist lam; - val lhs = list_ccomb (con, bound_vars (length vars)); - val appl = bind_fun vars (lhs == rhs); - val cs = ContProc.cont_thms lam; - val betas = map (fn c => mk_meta_eq (c RS beta_cfun)) cs; - in pg (def::betas) appl (K [rtac reflexive_thm 1]) end; -end; - -val _ = trace "Proving when_appl..."; -val when_appl = appl_of_def ax_when_def; -val _ = trace "Proving con_appls..."; -val con_appls = map appl_of_def axs_con_def; - -local - fun arg2typ n arg = - let val t = TVar (("'a", n), pcpoS) - in (n + 1, if is_lazy arg then mk_uT t else t) end; - - fun args2typ n [] = (n, oneT) - | args2typ n [arg] = arg2typ n arg - | args2typ n (arg::args) = - let - val (n1, t1) = arg2typ n arg; - val (n2, t2) = args2typ n1 args - in (n2, mk_sprodT (t1, t2)) end; - - fun cons2typ n [] = (n,oneT) - | cons2typ n [con] = args2typ n (snd con) - | cons2typ n (con::cons) = - let - val (n1, t1) = args2typ n (snd con); - val (n2, t2) = cons2typ n1 cons - in (n2, mk_ssumT (t1, t2)) end; -in - fun cons2ctyp cons = ctyp_of thy (snd (cons2typ 1 cons)); -end; - -local - val iso_swap = iso_locale RS iso_iso_swap; - fun one_con (con, args) = - let - val vns = map vname args; - val eqn = %:x_name === con_app2 con %: vns; - val conj = foldr1 mk_conj (eqn :: map (defined o %:) (nonlazy args)); - in Library.foldr mk_ex (vns, conj) end; - - val conj_assoc = @{thm conj_assoc}; - val exh = foldr1 mk_disj ((%:x_name === UU) :: map one_con cons); - val thm1 = instantiate' [SOME (cons2ctyp cons)] [] exh_start; - val thm2 = rewrite_rule (map mk_meta_eq ex_defined_iffs) thm1; - val thm3 = rewrite_rule [mk_meta_eq @{thm conj_assoc}] thm2; - - (* first 3 rules replace "x = UU \/ P" with "rep$x = UU \/ P" *) - val tacs = [ - rtac disjE 1, - etac (rep_defin' RS disjI1) 2, - etac disjI2 2, - rewrite_goals_tac [mk_meta_eq iso_swap], - rtac thm3 1]; -in - val _ = trace " Proving exhaust..."; - val exhaust = pg con_appls (mk_trp exh) (K tacs); - val _ = trace " Proving casedist..."; - val casedist = - standard (rewrite_rule exh_casedists (exhaust RS exh_casedist0)); -end; - -local - fun bind_fun t = Library.foldr mk_All (when_funs cons, t); - fun bound_fun i _ = Bound (length cons - i); - val when_app = list_ccomb (%%:(dname^"_when"), mapn bound_fun 1 cons); -in - val _ = trace " Proving when_strict..."; - val when_strict = - let - val axs = [when_appl, mk_meta_eq rep_strict]; - val goal = bind_fun (mk_trp (strict when_app)); - val tacs = [resolve_tac [sscase1, ssplit1, strictify1] 1]; - in pg axs goal (K tacs) end; - - val _ = trace " Proving when_apps..."; - val when_apps = - let - fun one_when n (con,args) = - let - val axs = when_appl :: con_appls; - val goal = bind_fun (lift_defined %: (nonlazy args, - mk_trp (when_app`(con_app con args) === - list_ccomb (bound_fun n 0, map %# args)))); - val tacs = [asm_simp_tac (HOLCF_ss addsimps [ax_abs_iso]) 1]; - in pg axs goal (K tacs) end; - in mapn one_when 1 cons end; -end; -val when_rews = when_strict :: when_apps; - -(* ----- theorems concerning the constructors, discriminators and selectors - *) - -local - fun dis_strict (con, _) = - let - val goal = mk_trp (strict (%%:(dis_name con))); - in pg axs_dis_def goal (K [rtac when_strict 1]) end; - - fun dis_app c (con, args) = - let - val lhs = %%:(dis_name c) ` con_app con args; - val rhs = if con = c then TT else FF; - val goal = lift_defined %: (nonlazy args, mk_trp (lhs === rhs)); - val tacs = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1]; - in pg axs_dis_def goal (K tacs) end; - - val _ = trace " Proving dis_apps..."; - val dis_apps = maps (fn (c,_) => map (dis_app c) cons) cons; - - fun dis_defin (con, args) = - let - val goal = defined (%:x_name) ==> defined (%%:(dis_name con) `% x_name); - val tacs = - [rtac casedist 1, - contr_tac 1, - DETERM_UNTIL_SOLVED (CHANGED - (asm_simp_tac (HOLCF_ss addsimps dis_apps) 1))]; - in pg [] goal (K tacs) end; - - val _ = trace " Proving dis_stricts..."; - val dis_stricts = map dis_strict cons; - val _ = trace " Proving dis_defins..."; - val dis_defins = map dis_defin cons; -in - val dis_rews = dis_stricts @ dis_defins @ dis_apps; -end; - -local - fun mat_strict (con, _) = - let - val goal = mk_trp (%%:(mat_name con) ` UU ` %:"rhs" === UU); - val tacs = [asm_simp_tac (HOLCF_ss addsimps [when_strict]) 1]; - in pg axs_mat_def goal (K tacs) end; - - val _ = trace " Proving mat_stricts..."; - val mat_stricts = map mat_strict cons; - - fun one_mat c (con, args) = - let - val lhs = %%:(mat_name c) ` con_app con args ` %:"rhs"; - val rhs = - if con = c - then list_ccomb (%:"rhs", map %# args) - else mk_fail; - val goal = lift_defined %: (nonlazy args, mk_trp (lhs === rhs)); - val tacs = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1]; - in pg axs_mat_def goal (K tacs) end; - - val _ = trace " Proving mat_apps..."; - val mat_apps = - maps (fn (c,_) => map (one_mat c) cons) cons; -in - val mat_rews = mat_stricts @ mat_apps; -end; - -local - fun ps args = mapn (fn n => fn _ => %:("pat" ^ string_of_int n)) 1 args; - - fun pat_lhs (con,args) = mk_branch (list_comb (%%:(pat_name con), ps args)); - - fun pat_rhs (con,[]) = mk_return ((%:"rhs") ` HOLogic.unit) - | pat_rhs (con,args) = - (mk_branch (mk_ctuple_pat (ps args))) - `(%:"rhs")`(mk_ctuple (map %# args)); - - fun pat_strict c = - let - val axs = @{thm branch_def} :: axs_pat_def; - val goal = mk_trp (strict (pat_lhs c ` (%:"rhs"))); - val tacs = [simp_tac (HOLCF_ss addsimps [when_strict]) 1]; - in pg axs goal (K tacs) end; - - fun pat_app c (con, args) = - let - val axs = @{thm branch_def} :: axs_pat_def; - val lhs = (pat_lhs c)`(%:"rhs")`(con_app con args); - val rhs = if con = fst c then pat_rhs c else mk_fail; - val goal = lift_defined %: (nonlazy args, mk_trp (lhs === rhs)); - val tacs = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1]; - in pg axs goal (K tacs) end; - - val _ = trace " Proving pat_stricts..."; - val pat_stricts = map pat_strict cons; - val _ = trace " Proving pat_apps..."; - val pat_apps = maps (fn c => map (pat_app c) cons) cons; -in - val pat_rews = pat_stricts @ pat_apps; -end; - -local - fun con_strict (con, args) = - let - val rules = abs_strict :: @{thms con_strict_rules}; - fun one_strict vn = - let - fun f arg = if vname arg = vn then UU else %# arg; - val goal = mk_trp (con_app2 con f args === UU); - val tacs = [simp_tac (HOL_basic_ss addsimps rules) 1]; - in pg con_appls goal (K tacs) end; - in map one_strict (nonlazy args) end; - - fun con_defin (con, args) = - let - fun iff_disj (t, []) = HOLogic.mk_not t - | iff_disj (t, ts) = t === foldr1 HOLogic.mk_disj ts; - val lhs = con_app con args === UU; - val rhss = map (fn x => %:x === UU) (nonlazy args); - val goal = mk_trp (iff_disj (lhs, rhss)); - val rule1 = iso_locale RS @{thm iso.abs_defined_iff}; - val rules = rule1 :: @{thms con_defined_iff_rules}; - val tacs = [simp_tac (HOL_ss addsimps rules) 1]; - in pg con_appls goal (K tacs) end; -in - val _ = trace " Proving con_stricts..."; - val con_stricts = maps con_strict cons; - val _ = trace " Proving con_defins..."; - val con_defins = map con_defin cons; - val con_rews = con_stricts @ con_defins; -end; - -local - val rules = - [compact_sinl, compact_sinr, compact_spair, compact_up, compact_ONE]; - fun con_compact (con, args) = - let - val concl = mk_trp (mk_compact (con_app con args)); - val goal = lift (fn x => mk_compact (%#x)) (args, concl); - val tacs = [ - rtac (iso_locale RS iso_compact_abs) 1, - REPEAT (resolve_tac rules 1 ORELSE atac 1)]; - in pg con_appls goal (K tacs) end; -in - val _ = trace " Proving con_compacts..."; - val con_compacts = map con_compact cons; -end; - -local - fun one_sel sel = - pg axs_sel_def (mk_trp (strict (%%:sel))) - (K [simp_tac (HOLCF_ss addsimps when_rews) 1]); - - fun sel_strict (_, args) = - List.mapPartial (Option.map one_sel o sel_of) args; -in - val _ = trace " Proving sel_stricts..."; - val sel_stricts = maps sel_strict cons; -end; - -local - fun sel_app_same c n sel (con, args) = - let - val nlas = nonlazy args; - val vns = map vname args; - val vnn = List.nth (vns, n); - val nlas' = List.filter (fn v => v <> vnn) nlas; - val lhs = (%%:sel)`(con_app con args); - val goal = lift_defined %: (nlas', mk_trp (lhs === %:vnn)); - fun tacs1 ctxt = - if vnn mem nlas - then [case_UU_tac ctxt (when_rews @ con_stricts) 1 vnn] - else []; - val tacs2 = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1]; - in pg axs_sel_def goal (fn ctxt => (tacs1 ctxt @ tacs2)) end; - - fun sel_app_diff c n sel (con, args) = - let - val nlas = nonlazy args; - val goal = mk_trp (%%:sel ` con_app con args === UU); - fun tacs1 ctxt = map (case_UU_tac ctxt (when_rews @ con_stricts) 1) nlas; - val tacs2 = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1]; - in pg axs_sel_def goal (fn ctxt => (tacs1 ctxt @ tacs2)) end; - - fun sel_app c n sel (con, args) = - if con = c - then sel_app_same c n sel (con, args) - else sel_app_diff c n sel (con, args); - - fun one_sel c n sel = map (sel_app c n sel) cons; - fun one_sel' c n arg = Option.map (one_sel c n) (sel_of arg); - fun one_con (c, args) = - flat (map_filter I (mapn (one_sel' c) 0 args)); -in - val _ = trace " Proving sel_apps..."; - val sel_apps = maps one_con cons; -end; - -local - fun sel_defin sel = - let - val goal = defined (%:x_name) ==> defined (%%:sel`%x_name); - val tacs = [ - rtac casedist 1, - contr_tac 1, - DETERM_UNTIL_SOLVED (CHANGED - (asm_simp_tac (HOLCF_ss addsimps sel_apps) 1))]; - in pg [] goal (K tacs) end; -in - val _ = trace " Proving sel_defins..."; - val sel_defins = - if length cons = 1 - then List.mapPartial (fn arg => Option.map sel_defin (sel_of arg)) - (filter_out is_lazy (snd (hd cons))) - else []; -end; - -val sel_rews = sel_stricts @ sel_defins @ sel_apps; - -val _ = trace " Proving dist_les..."; -val distincts_le = - let - fun dist (con1, args1) (con2, args2) = - let - val goal = lift_defined %: (nonlazy args1, - mk_trp (con_app con1 args1 ~<< con_app con2 args2)); - fun tacs ctxt = [ - rtac @{thm rev_contrapos} 1, - eres_inst_tac ctxt [(("f", 0), dis_name con1)] monofun_cfun_arg 1] - @ map (case_UU_tac ctxt (con_stricts @ dis_rews) 1) (nonlazy args2) - @ [asm_simp_tac (HOLCF_ss addsimps dis_rews) 1]; - in pg [] goal tacs end; - - fun distinct (con1, args1) (con2, args2) = - let - val arg1 = (con1, args1); - val arg2 = - (con2, ListPair.map (fn (arg,vn) => upd_vname (K vn) arg) - (args2, Name.variant_list (map vname args1) (map vname args2))); - in [dist arg1 arg2, dist arg2 arg1] end; - fun distincts [] = [] - | distincts (c::cs) = (map (distinct c) cs) :: distincts cs; - in distincts cons end; -val dist_les = flat (flat distincts_le); - -val _ = trace " Proving dist_eqs..."; -val dist_eqs = - let - fun distinct (_,args1) ((_,args2), leqs) = - let - val (le1,le2) = (hd leqs, hd(tl leqs)); - val (eq1,eq2) = (le1 RS dist_eqI, le2 RS dist_eqI) - in - if nonlazy args1 = [] then [eq1, eq1 RS not_sym] else - if nonlazy args2 = [] then [eq2, eq2 RS not_sym] else - [eq1, eq2] - end; - fun distincts [] = [] - | distincts ((c,leqs)::cs) = - flat - (ListPair.map (distinct c) ((map #1 cs),leqs)) @ - distincts cs; - in map standard (distincts (cons ~~ distincts_le)) end; - -local - fun pgterm rel con args = - let - fun append s = upd_vname (fn v => v^s); - val (largs, rargs) = (args, map (append "'") args); - val concl = - foldr1 mk_conj (ListPair.map rel (map %# largs, map %# rargs)); - val prem = rel (con_app con largs, con_app con rargs); - val sargs = case largs of [_] => [] | _ => nonlazy args; - val prop = lift_defined %: (sargs, mk_trp (prem === concl)); - in pg con_appls prop end; - val cons' = List.filter (fn (_,args) => args<>[]) cons; -in - val _ = trace " Proving inverts..."; - val inverts = - let - val abs_less = ax_abs_iso RS (allI RS injection_less); - val tacs = - [asm_full_simp_tac (HOLCF_ss addsimps [abs_less, spair_less]) 1]; - in map (fn (con, args) => pgterm (op <<) con args (K tacs)) cons' end; - - val _ = trace " Proving injects..."; - val injects = - let - val abs_eq = ax_abs_iso RS (allI RS injection_eq); - val tacs = [asm_full_simp_tac (HOLCF_ss addsimps [abs_eq, spair_eq]) 1]; - in map (fn (con, args) => pgterm (op ===) con args (K tacs)) cons' end; -end; - -(* ----- theorems concerning one induction step ----------------------------- *) - -val copy_strict = - let - val _ = trace " Proving copy_strict..."; - val goal = mk_trp (strict (dc_copy `% "f")); - val rules = [abs_strict, rep_strict] @ @{thms domain_fun_stricts}; - val tacs = [asm_simp_tac (HOLCF_ss addsimps rules) 1]; - in pg [ax_copy_def] goal (K tacs) end; - -local - fun copy_app (con, args) = - let - val lhs = dc_copy`%"f"`(con_app con args); - fun one_rhs arg = - if DatatypeAux.is_rec_type (dtyp_of arg) - then Domain_Axioms.copy_of_dtyp (cproj (%:"f") eqs) (dtyp_of arg) ` (%# arg) - else (%# arg); - val rhs = con_app2 con one_rhs args; - val goal = lift_defined %: (nonlazy_rec args, mk_trp (lhs === rhs)); - val args' = List.filter (fn a => not (is_rec a orelse is_lazy a)) args; - val stricts = abs_strict :: rep_strict :: @{thms domain_fun_stricts}; - fun tacs1 ctxt = map (case_UU_tac ctxt stricts 1 o vname) args'; - val rules = [ax_abs_iso] @ @{thms domain_fun_simps}; - val tacs2 = [asm_simp_tac (HOLCF_ss addsimps rules) 1]; - in pg (ax_copy_def::con_appls) goal (fn ctxt => (tacs1 ctxt @ tacs2)) end; -in - val _ = trace " Proving copy_apps..."; - val copy_apps = map copy_app cons; -end; - -local - fun one_strict (con, args) = - let - val goal = mk_trp (dc_copy`UU`(con_app con args) === UU); - val rews = copy_strict :: copy_apps @ con_rews; - fun tacs ctxt = map (case_UU_tac ctxt rews 1) (nonlazy args) @ - [asm_simp_tac (HOLCF_ss addsimps rews) 1]; - in pg [] goal tacs end; - - fun has_nonlazy_rec (_, args) = exists is_nonlazy_rec args; -in - val _ = trace " Proving copy_stricts..."; - val copy_stricts = map one_strict (List.filter has_nonlazy_rec cons); -end; - -val copy_rews = copy_strict :: copy_apps @ copy_stricts; - -in - thy - |> Sign.add_path (Long_Name.base_name dname) - |> snd o PureThy.add_thmss [ - ((Binding.name "iso_rews" , iso_rews ), [Simplifier.simp_add]), - ((Binding.name "exhaust" , [exhaust] ), []), - ((Binding.name "casedist" , [casedist] ), [Induct.cases_type dname]), - ((Binding.name "when_rews" , when_rews ), [Simplifier.simp_add]), - ((Binding.name "compacts" , con_compacts), [Simplifier.simp_add]), - ((Binding.name "con_rews" , con_rews ), [Simplifier.simp_add]), - ((Binding.name "sel_rews" , sel_rews ), [Simplifier.simp_add]), - ((Binding.name "dis_rews" , dis_rews ), [Simplifier.simp_add]), - ((Binding.name "pat_rews" , pat_rews ), [Simplifier.simp_add]), - ((Binding.name "dist_les" , dist_les ), [Simplifier.simp_add]), - ((Binding.name "dist_eqs" , dist_eqs ), [Simplifier.simp_add]), - ((Binding.name "inverts" , inverts ), [Simplifier.simp_add]), - ((Binding.name "injects" , injects ), [Simplifier.simp_add]), - ((Binding.name "copy_rews" , copy_rews ), [Simplifier.simp_add]), - ((Binding.name "match_rews", mat_rews ), [Simplifier.simp_add])] - |> Sign.parent_path - |> pair (iso_rews @ when_rews @ con_rews @ sel_rews @ dis_rews @ - pat_rews @ dist_les @ dist_eqs @ copy_rews) -end; (* let *) - -fun comp_theorems (comp_dnam, eqs: eq list) thy = -let -val global_ctxt = ProofContext.init thy; - -val dnames = map (fst o fst) eqs; -val conss = map snd eqs; -val comp_dname = Sign.full_bname thy comp_dnam; - -val _ = message ("Proving induction properties of domain "^comp_dname^" ..."); -val pg = pg' thy; - -(* ----- getting the composite axiom and definitions ------------------------ *) - -local - fun ga s dn = PureThy.get_thm thy (dn ^ "." ^ s); -in - val axs_reach = map (ga "reach" ) dnames; - val axs_take_def = map (ga "take_def" ) dnames; - val axs_finite_def = map (ga "finite_def") dnames; - val ax_copy2_def = ga "copy_def" comp_dnam; - val ax_bisim_def = ga "bisim_def" comp_dnam; -end; - -local - fun gt s dn = PureThy.get_thm thy (dn ^ "." ^ s); - fun gts s dn = PureThy.get_thms thy (dn ^ "." ^ s); -in - val cases = map (gt "casedist" ) dnames; - val con_rews = maps (gts "con_rews" ) dnames; - val copy_rews = maps (gts "copy_rews") dnames; -end; - -fun dc_take dn = %%:(dn^"_take"); -val x_name = idx_name dnames "x"; -val P_name = idx_name dnames "P"; -val n_eqs = length eqs; - -(* ----- theorems concerning finite approximation and finite induction ------ *) - -local - val iterate_Cprod_ss = simpset_of @{theory Fix}; - val copy_con_rews = copy_rews @ con_rews; - val copy_take_defs = - (if n_eqs = 1 then [] else [ax_copy2_def]) @ axs_take_def; - val _ = trace " Proving take_stricts..."; - val take_stricts = - let - fun one_eq ((dn, args), _) = strict (dc_take dn $ %:"n"); - val goal = mk_trp (foldr1 mk_conj (map one_eq eqs)); - fun tacs ctxt = [ - InductTacs.induct_tac ctxt [[SOME "n"]] 1, - simp_tac iterate_Cprod_ss 1, - asm_simp_tac (iterate_Cprod_ss addsimps copy_rews) 1]; - in pg copy_take_defs goal tacs end; - - val take_stricts' = rewrite_rule copy_take_defs take_stricts; - fun take_0 n dn = - let - val goal = mk_trp ((dc_take dn $ %%:"HOL.zero") `% x_name n === UU); - in pg axs_take_def goal (K [simp_tac iterate_Cprod_ss 1]) end; - val take_0s = mapn take_0 1 dnames; - fun c_UU_tac ctxt = case_UU_tac ctxt (take_stricts'::copy_con_rews) 1; - val _ = trace " Proving take_apps..."; - val take_apps = - let - fun mk_eqn dn (con, args) = - let - fun mk_take n = dc_take (List.nth (dnames, n)) $ %:"n"; - fun one_rhs arg = - if DatatypeAux.is_rec_type (dtyp_of arg) - then Domain_Axioms.copy_of_dtyp mk_take (dtyp_of arg) ` (%# arg) - else (%# arg); - val lhs = (dc_take dn $ (%%:"Suc" $ %:"n"))`(con_app con args); - val rhs = con_app2 con one_rhs args; - in Library.foldr mk_all (map vname args, lhs === rhs) end; - fun mk_eqns ((dn, _), cons) = map (mk_eqn dn) cons; - val goal = mk_trp (foldr1 mk_conj (maps mk_eqns eqs)); - val simps = List.filter (has_fewer_prems 1) copy_rews; - fun con_tac ctxt (con, args) = - if nonlazy_rec args = [] - then all_tac - else EVERY (map (c_UU_tac ctxt) (nonlazy_rec args)) THEN - asm_full_simp_tac (HOLCF_ss addsimps copy_rews) 1; - fun eq_tacs ctxt ((dn, _), cons) = map (con_tac ctxt) cons; - fun tacs ctxt = - simp_tac iterate_Cprod_ss 1 :: - InductTacs.induct_tac ctxt [[SOME "n"]] 1 :: - simp_tac (iterate_Cprod_ss addsimps copy_con_rews) 1 :: - asm_full_simp_tac (HOLCF_ss addsimps simps) 1 :: - TRY (safe_tac HOL_cs) :: - maps (eq_tacs ctxt) eqs; - in pg copy_take_defs goal tacs end; -in - val take_rews = map standard - (atomize global_ctxt take_stricts @ take_0s @ atomize global_ctxt take_apps); -end; (* local *) - -local - fun one_con p (con,args) = - let - fun ind_hyp arg = %:(P_name (1 + rec_of arg)) $ bound_arg args arg; - val t1 = mk_trp (%:p $ con_app2 con (bound_arg args) args); - val t2 = lift ind_hyp (List.filter is_rec args, t1); - val t3 = lift_defined (bound_arg (map vname args)) (nonlazy args, t2); - in Library.foldr mk_All (map vname args, t3) end; - - fun one_eq ((p, cons), concl) = - mk_trp (%:p $ UU) ===> Logic.list_implies (map (one_con p) cons, concl); - - fun ind_term concf = Library.foldr one_eq - (mapn (fn n => fn x => (P_name n, x)) 1 conss, - mk_trp (foldr1 mk_conj (mapn concf 1 dnames))); - val take_ss = HOL_ss addsimps take_rews; - fun quant_tac ctxt i = EVERY - (mapn (fn n => fn _ => res_inst_tac ctxt [(("x", 0), x_name n)] spec i) 1 dnames); - - fun ind_prems_tac prems = EVERY - (maps (fn cons => - (resolve_tac prems 1 :: - maps (fn (_,args) => - resolve_tac prems 1 :: - map (K(atac 1)) (nonlazy args) @ - map (K(atac 1)) (List.filter is_rec args)) - cons)) - conss); - local - (* check whether every/exists constructor of the n-th part of the equation: - it has a possibly indirectly recursive argument that isn't/is possibly - indirectly lazy *) - fun rec_to quant nfn rfn ns lazy_rec (n,cons) = quant (exists (fn arg => - is_rec arg andalso not(rec_of arg mem ns) andalso - ((rec_of arg = n andalso nfn(lazy_rec orelse is_lazy arg)) orelse - rec_of arg <> n andalso rec_to quant nfn rfn (rec_of arg::ns) - (lazy_rec orelse is_lazy arg) (n, (List.nth(conss,rec_of arg)))) - ) o snd) cons; - fun all_rec_to ns = rec_to forall not all_rec_to ns; - fun warn (n,cons) = - if all_rec_to [] false (n,cons) - then (warning ("domain "^List.nth(dnames,n)^" is empty!"); true) - else false; - fun lazy_rec_to ns = rec_to exists I lazy_rec_to ns; - - in - val n__eqs = mapn (fn n => fn (_,cons) => (n,cons)) 0 eqs; - val is_emptys = map warn n__eqs; - val is_finite = forall (not o lazy_rec_to [] false) n__eqs; - end; -in (* local *) - val _ = trace " Proving finite_ind..."; - val finite_ind = - let - fun concf n dn = %:(P_name n) $ (dc_take dn $ %:"n" `%(x_name n)); - val goal = ind_term concf; - - fun tacf {prems, context} = - let - val tacs1 = [ - quant_tac context 1, - simp_tac HOL_ss 1, - InductTacs.induct_tac context [[SOME "n"]] 1, - simp_tac (take_ss addsimps prems) 1, - TRY (safe_tac HOL_cs)]; - fun arg_tac arg = - case_UU_tac context (prems @ con_rews) 1 - (List.nth (dnames, rec_of arg) ^ "_take n$" ^ vname arg); - fun con_tacs (con, args) = - asm_simp_tac take_ss 1 :: - map arg_tac (List.filter is_nonlazy_rec args) @ - [resolve_tac prems 1] @ - map (K (atac 1)) (nonlazy args) @ - map (K (etac spec 1)) (List.filter is_rec args); - fun cases_tacs (cons, cases) = - res_inst_tac context [(("x", 0), "x")] cases 1 :: - asm_simp_tac (take_ss addsimps prems) 1 :: - maps con_tacs cons; - in - tacs1 @ maps cases_tacs (conss ~~ cases) - end; - in pg'' thy [] goal tacf - handle ERROR _ => (warning "Proof of finite_ind failed."; TrueI) - end; - - val _ = trace " Proving take_lemmas..."; - val take_lemmas = - let - fun take_lemma n (dn, ax_reach) = - let - val lhs = dc_take dn $ Bound 0 `%(x_name n); - val rhs = dc_take dn $ Bound 0 `%(x_name n^"'"); - val concl = mk_trp (%:(x_name n) === %:(x_name n^"'")); - val goal = mk_All ("n", mk_trp (lhs === rhs)) ===> concl; - fun tacf {prems, context} = [ - res_inst_tac context [(("t", 0), x_name n )] (ax_reach RS subst) 1, - res_inst_tac context [(("t", 0), x_name n^"'")] (ax_reach RS subst) 1, - stac fix_def2 1, - REPEAT (CHANGED - (rtac (contlub_cfun_arg RS ssubst) 1 THEN chain_tac 1)), - stac contlub_cfun_fun 1, - stac contlub_cfun_fun 2, - rtac lub_equal 3, - chain_tac 1, - rtac allI 1, - resolve_tac prems 1]; - in pg'' thy axs_take_def goal tacf end; - in mapn take_lemma 1 (dnames ~~ axs_reach) end; - -(* ----- theorems concerning finiteness and induction ----------------------- *) - - val _ = trace " Proving finites, ind..."; - val (finites, ind) = - ( - if is_finite - then (* finite case *) - let - fun take_enough dn = mk_ex ("n",dc_take dn $ Bound 0 ` %:"x" === %:"x"); - fun dname_lemma dn = - let - val prem1 = mk_trp (defined (%:"x")); - val disj1 = mk_all ("n", dc_take dn $ Bound 0 ` %:"x" === UU); - val prem2 = mk_trp (mk_disj (disj1, take_enough dn)); - val concl = mk_trp (take_enough dn); - val goal = prem1 ===> prem2 ===> concl; - val tacs = [ - etac disjE 1, - etac notE 1, - resolve_tac take_lemmas 1, - asm_simp_tac take_ss 1, - atac 1]; - in pg [] goal (K tacs) end; - val _ = trace " Proving finite_lemmas1a"; - val finite_lemmas1a = map dname_lemma dnames; - - val _ = trace " Proving finite_lemma1b"; - val finite_lemma1b = - let - fun mk_eqn n ((dn, args), _) = - let - val disj1 = dc_take dn $ Bound 1 ` Bound 0 === UU; - val disj2 = dc_take dn $ Bound 1 ` Bound 0 === Bound 0; - in - mk_constrainall - (x_name n, Type (dn,args), mk_disj (disj1, disj2)) - end; - val goal = - mk_trp (mk_all ("n", foldr1 mk_conj (mapn mk_eqn 1 eqs))); - fun arg_tacs ctxt vn = [ - eres_inst_tac ctxt [(("x", 0), vn)] all_dupE 1, - etac disjE 1, - asm_simp_tac (HOL_ss addsimps con_rews) 1, - asm_simp_tac take_ss 1]; - fun con_tacs ctxt (con, args) = - asm_simp_tac take_ss 1 :: - maps (arg_tacs ctxt) (nonlazy_rec args); - fun foo_tacs ctxt n (cons, cases) = - simp_tac take_ss 1 :: - rtac allI 1 :: - res_inst_tac ctxt [(("x", 0), x_name n)] cases 1 :: - asm_simp_tac take_ss 1 :: - maps (con_tacs ctxt) cons; - fun tacs ctxt = - rtac allI 1 :: - InductTacs.induct_tac ctxt [[SOME "n"]] 1 :: - simp_tac take_ss 1 :: - TRY (safe_tac (empty_cs addSEs [conjE] addSIs [conjI])) :: - flat (mapn (foo_tacs ctxt) 1 (conss ~~ cases)); - in pg [] goal tacs end; - - fun one_finite (dn, l1b) = - let - val goal = mk_trp (%%:(dn^"_finite") $ %:"x"); - fun tacs ctxt = [ - case_UU_tac ctxt take_rews 1 "x", - eresolve_tac finite_lemmas1a 1, - step_tac HOL_cs 1, - step_tac HOL_cs 1, - cut_facts_tac [l1b] 1, - fast_tac HOL_cs 1]; - in pg axs_finite_def goal tacs end; - - val _ = trace " Proving finites"; - val finites = map one_finite (dnames ~~ atomize global_ctxt finite_lemma1b); - val _ = trace " Proving ind"; - val ind = - let - fun concf n dn = %:(P_name n) $ %:(x_name n); - fun tacf {prems, context} = - let - fun finite_tacs (finite, fin_ind) = [ - rtac(rewrite_rule axs_finite_def finite RS exE)1, - etac subst 1, - rtac fin_ind 1, - ind_prems_tac prems]; - in - TRY (safe_tac HOL_cs) :: - maps finite_tacs (finites ~~ atomize global_ctxt finite_ind) - end; - in pg'' thy [] (ind_term concf) tacf end; - in (finites, ind) end (* let *) - - else (* infinite case *) - let - fun one_finite n dn = - read_instantiate global_ctxt [(("P", 0), dn ^ "_finite " ^ x_name n)] excluded_middle; - val finites = mapn one_finite 1 dnames; - - val goal = - let - fun one_adm n _ = mk_trp (mk_adm (%:(P_name n))); - fun concf n dn = %:(P_name n) $ %:(x_name n); - in Logic.list_implies (mapn one_adm 1 dnames, ind_term concf) end; - fun tacf {prems, context} = - map (fn ax_reach => rtac (ax_reach RS subst) 1) axs_reach @ [ - quant_tac context 1, - rtac (adm_impl_admw RS wfix_ind) 1, - REPEAT_DETERM (rtac adm_all 1), - REPEAT_DETERM ( - TRY (rtac adm_conj 1) THEN - rtac adm_subst 1 THEN - cont_tacR 1 THEN resolve_tac prems 1), - strip_tac 1, - rtac (rewrite_rule axs_take_def finite_ind) 1, - ind_prems_tac prems]; - val ind = (pg'' thy [] goal tacf - handle ERROR _ => - (warning "Cannot prove infinite induction rule"; refl)); - in (finites, ind) end - ) - handle THM _ => - (warning "Induction proofs failed (THM raised)."; ([], TrueI)) - | ERROR _ => - (warning "Induction proofs failed (ERROR raised)."; ([], TrueI)); - - -end; (* local *) - -(* ----- theorem concerning coinduction ------------------------------------- *) - -local - val xs = mapn (fn n => K (x_name n)) 1 dnames; - fun bnd_arg n i = Bound(2*(n_eqs - n)-i-1); - val take_ss = HOL_ss addsimps take_rews; - val sproj = prj (fn s => K("fst("^s^")")) (fn s => K("snd("^s^")")); - val _ = trace " Proving coind_lemma..."; - val coind_lemma = - let - fun mk_prj n _ = proj (%:"R") eqs n $ bnd_arg n 0 $ bnd_arg n 1; - fun mk_eqn n dn = - (dc_take dn $ %:"n" ` bnd_arg n 0) === - (dc_take dn $ %:"n" ` bnd_arg n 1); - fun mk_all2 (x,t) = mk_all (x, mk_all (x^"'", t)); - val goal = - mk_trp (mk_imp (%%:(comp_dname^"_bisim") $ %:"R", - Library.foldr mk_all2 (xs, - Library.foldr mk_imp (mapn mk_prj 0 dnames, - foldr1 mk_conj (mapn mk_eqn 0 dnames))))); - fun x_tacs ctxt n x = [ - rotate_tac (n+1) 1, - etac all2E 1, - eres_inst_tac ctxt [(("P", 1), sproj "R" eqs n^" "^x^" "^x^"'")] (mp RS disjE) 1, - TRY (safe_tac HOL_cs), - REPEAT (CHANGED (asm_simp_tac take_ss 1))]; - fun tacs ctxt = [ - rtac impI 1, - InductTacs.induct_tac ctxt [[SOME "n"]] 1, - simp_tac take_ss 1, - safe_tac HOL_cs] @ - flat (mapn (x_tacs ctxt) 0 xs); - in pg [ax_bisim_def] goal tacs end; -in - val _ = trace " Proving coind..."; - val coind = - let - fun mk_prj n x = mk_trp (proj (%:"R") eqs n $ %:x $ %:(x^"'")); - fun mk_eqn x = %:x === %:(x^"'"); - val goal = - mk_trp (%%:(comp_dname^"_bisim") $ %:"R") ===> - Logic.list_implies (mapn mk_prj 0 xs, - mk_trp (foldr1 mk_conj (map mk_eqn xs))); - val tacs = - TRY (safe_tac HOL_cs) :: - maps (fn take_lemma => [ - rtac take_lemma 1, - cut_facts_tac [coind_lemma] 1, - fast_tac HOL_cs 1]) - take_lemmas; - in pg [] goal (K tacs) end; -end; (* local *) - -val inducts = ProjectRule.projections (ProofContext.init thy) ind; -fun ind_rule (dname, rule) = ((Binding.empty, [rule]), [Induct.induct_type dname]); -val induct_failed = (Thm.prop_of ind = Thm.prop_of TrueI); - -in thy |> Sign.add_path comp_dnam - |> snd o PureThy.add_thmss [ - ((Binding.name "take_rews" , take_rews ), [Simplifier.simp_add]), - ((Binding.name "take_lemmas", take_lemmas ), []), - ((Binding.name "finites" , finites ), []), - ((Binding.name "finite_ind" , [finite_ind]), []), - ((Binding.name "ind" , [ind] ), []), - ((Binding.name "coind" , [coind] ), [])] - |> (if induct_failed then I - else snd o PureThy.add_thmss (map ind_rule (dnames ~~ inducts))) - |> Sign.parent_path |> pair take_rews -end; (* let *) -end; (* local *) -end; (* struct *) diff -r 6da9c2a49fed -r 631546213601 src/Pure/Isar/class.ML --- a/src/Pure/Isar/class.ML Tue Jul 21 14:08:58 2009 +0200 +++ b/src/Pure/Isar/class.ML Tue Jul 21 17:02:18 2009 +0200 @@ -68,9 +68,8 @@ val base_morph = inst_morph $> Morphism.binding_morphism (Binding.prefix false (class_prefix class)) $> Element.satisfy_morphism (the_list wit); - val defs = these_defs thy sups; - val eq_morph = Element.eq_morphism thy defs; - val morph = base_morph $> eq_morph; + val eqs = these_defs thy sups; + val eq_morph = Element.eq_morphism thy eqs; (* assm_intro *) fun prove_assm_intro thm = @@ -97,7 +96,7 @@ ORELSE' Tactic.assume_tac)); val of_class = SkipProof.prove_global thy [] [] of_class_prop (K tac); - in (base_morph, morph, export_morph, axiom, assm_intro, of_class) end; + in (base_morph, eqs, export_morph, axiom, assm_intro, of_class) end; (* reading and processing class specifications *) @@ -284,9 +283,8 @@ ||> Theory.checkpoint |-> (fn (param_map, params, assm_axiom) => `(fn thy => calculate thy class sups base_sort param_map assm_axiom) - #-> (fn (base_morph, morph, export_morph, axiom, assm_intro, of_class) => - Locale.add_registration (class, (morph, export_morph)) - #> Context.theory_map (Locale.activate_facts (class, morph $> export_morph)) + #-> (fn (base_morph, eqs, export_morph, axiom, assm_intro, of_class) => + Locale.add_registration_eqs (class, base_morph) eqs export_morph #> register class sups params base_sort base_morph axiom assm_intro of_class)) |> TheoryTarget.init (SOME class) |> pair class diff -r 6da9c2a49fed -r 631546213601 src/Pure/Isar/code.ML --- a/src/Pure/Isar/code.ML Tue Jul 21 14:08:58 2009 +0200 +++ b/src/Pure/Isar/code.ML Tue Jul 21 17:02:18 2009 +0200 @@ -801,7 +801,9 @@ of SOME T_class => T_class | _ => error ("Bad certificate: " ^ Display.string_of_thm thm); val tvar = case try Term.dest_TVar T - of SOME tvar => tvar + of SOME (tvar as (_, sort)) => if null (filter (can (AxClass.get_info thy)) sort) + then tvar + else error ("Bad sort: " ^ Display.string_of_thm thm) | _ => error ("Bad type: " ^ Display.string_of_thm thm); val _ = if Term.add_tvars eqn [] = [tvar] then () else error ("Inconsistent type: " ^ Display.string_of_thm thm); diff -r 6da9c2a49fed -r 631546213601 src/Pure/Isar/locale.ML --- a/src/Pure/Isar/locale.ML Tue Jul 21 14:08:58 2009 +0200 +++ b/src/Pure/Isar/locale.ML Tue Jul 21 17:02:18 2009 +0200 @@ -68,9 +68,8 @@ val intro_locales_tac: bool -> Proof.context -> thm list -> tactic (* Registrations and dependencies *) - val add_registration: string * (morphism * morphism) -> theory -> theory + val add_registration_eqs: string * morphism -> thm list -> morphism -> theory -> theory val amend_registration: morphism -> string * morphism -> theory -> theory - val add_registration_eqs: string * morphism -> thm list -> morphism -> theory -> theory val add_dependency: string -> string * morphism -> morphism -> theory -> theory (* Diagnostic *) @@ -295,8 +294,7 @@ fun activate_declarations dep = Context.proof_map (fn context => let val thy = Context.theory_of context; - val context' = roundup thy activate_decls dep (get_idents context, context) |-> put_idents; - in context' end); + in roundup thy activate_decls dep (get_idents context, context) |-> put_idents end); fun activate_facts dep context = let @@ -346,11 +344,6 @@ fun all_registrations thy = Registrations.get thy |> map reg_morph; -fun add_registration (name, (base_morph, export)) thy = - roundup thy (fn (name', morph') => Registrations.map (cons ((name', (morph', export)), stamp ()))) - (name, base_morph) (get_idents (Context.Theory thy), thy) - (* FIXME |-> (Context.theory_map o put_idents_diag)*) |> snd; - fun amend_registration morph (name, base_morph) thy = let val regs = map #1 (Registrations.get thy); @@ -373,8 +366,10 @@ val morph = if null eqns then proto_morph else proto_morph $> Element.eq_morphism thy eqns; in - thy - |> add_registration (dep, (morph, export)) + (get_idents (Context.Theory thy), thy) + |> roundup thy (fn (dep', morph') => + Registrations.map (cons ((dep', (morph', export)), stamp ()))) (dep, morph) + |> snd |> Context.theory_map (activate_facts (dep, morph $> export)) end; diff -r 6da9c2a49fed -r 631546213601 src/Pure/Syntax/syn_trans.ML --- a/src/Pure/Syntax/syn_trans.ML Tue Jul 21 14:08:58 2009 +0200 +++ b/src/Pure/Syntax/syn_trans.ML Tue Jul 21 17:02:18 2009 +0200 @@ -8,6 +8,8 @@ sig val eta_contract: bool ref val atomic_abs_tr': string * typ * term -> term * term + val preserve_binder_abs_tr': string -> string -> string * (term list -> term) + val preserve_binder_abs2_tr': string -> string -> string * (term list -> term) val mk_binder_tr: string * string -> string * (term list -> term) val mk_binder_tr': string * string -> string * (term list -> term) val dependent_tr': string * string -> term list -> term @@ -309,6 +311,14 @@ ([], _) => raise Ast.AST ("abs_ast_tr'", asts) | (xs, body) => Ast.Appl [Ast.Constant "_lambda", Ast.fold_ast "_pttrns" xs, body]); +fun preserve_binder_abs_tr' name syn = (name, fn (Abs abs :: ts) => + let val (x, t) = atomic_abs_tr' abs + in list_comb (Lexicon.const syn $ x $ t, ts) end); + +fun preserve_binder_abs2_tr' name syn = (name, fn (A :: Abs abs :: ts) => + let val (x, t) = atomic_abs_tr' abs + in list_comb (Lexicon.const syn $ x $ A $ t, ts) end); + (* binder *) diff -r 6da9c2a49fed -r 631546213601 src/Tools/Code/code_ml.ML --- a/src/Tools/Code/code_ml.ML Tue Jul 21 14:08:58 2009 +0200 +++ b/src/Tools/Code/code_ml.ML Tue Jul 21 17:02:18 2009 +0200 @@ -966,7 +966,7 @@ val sml_code = "let\n" ^ value_code ^ "\nin " ^ value_name' ^ space_implode " " (map (enclose "(" ")") args) ^ " end"; in ML_Context.evaluate ctxt false reff sml_code end; - in Code_Thingol.eval thy I postproc evaluator t end; + in Code_Thingol.eval thy postproc evaluator t end; (* instrumentalization by antiquotation *) diff -r 6da9c2a49fed -r 631546213601 src/Tools/Code/code_preproc.ML --- a/src/Tools/Code/code_preproc.ML Tue Jul 21 14:08:58 2009 +0200 +++ b/src/Tools/Code/code_preproc.ML Tue Jul 21 17:02:18 2009 +0200 @@ -23,9 +23,10 @@ val all: code_graph -> string list val pretty: theory -> code_graph -> Pretty.T val obtain: theory -> string list -> term list -> code_algebra * code_graph - val eval_conv: theory -> (sort -> sort) + val resubst_triv_consts: theory -> term -> term + val eval_conv: theory -> (code_algebra -> code_graph -> (string * sort) list -> term -> cterm -> thm) -> cterm -> thm - val eval: theory -> (sort -> sort) -> ((term -> term) -> 'a -> 'a) + val eval: theory -> ((term -> term) -> 'a -> 'a) -> (code_algebra -> code_graph -> (string * sort) list -> term -> 'a) -> term -> 'a val setup: theory -> theory @@ -161,7 +162,10 @@ |> rhs_conv (Simplifier.rewrite post) end; -fun postprocess_term thy = term_of_conv thy (postprocess_conv thy); +fun resubst_triv_consts thy = map_aterms (fn t as Const (c, ty) => Const (Code.resubst_alias thy c, ty) + | t => t); + +fun postprocess_term thy = term_of_conv thy (postprocess_conv thy) #> resubst_triv_consts thy; fun print_codeproc thy = let @@ -495,7 +499,7 @@ Abs (v, prepare_sorts_typ prep_sort ty, prepare_sorts prep_sort t) | prepare_sorts _ (t as Bound _) = t; -fun gen_eval thy cterm_of conclude_evaluation prep_sort evaluator proto_ct = +fun gen_eval thy cterm_of conclude_evaluation evaluator proto_ct = let val pp = Syntax.pp_global thy; val ct = cterm_of proto_ct; @@ -507,8 +511,10 @@ val vs = Term.add_tfrees t' []; val consts = fold_aterms (fn Const (c, _) => insert (op =) c | _ => I) t' []; - - val t'' = prepare_sorts prep_sort t'; + + val add_triv_classes = curry (Sorts.inter_sort (Sign.classes_of thy)) + (Code.triv_classes thy); + val t'' = prepare_sorts add_triv_classes t'; val (algebra', eqngr') = obtain thy consts [t'']; in conclude_evaluation (evaluator algebra' eqngr' vs t'' ct') thm end; @@ -527,8 +533,8 @@ end; in gen_eval thy I conclude_evaluation end; -fun eval thy prep_sort postproc evaluator = gen_eval thy (Thm.cterm_of thy) - (K o postproc (postprocess_term thy)) prep_sort (simple_evaluator evaluator); +fun eval thy postproc evaluator = gen_eval thy (Thm.cterm_of thy) + (K o postproc (postprocess_term thy)) (simple_evaluator evaluator); (** setup **) diff -r 6da9c2a49fed -r 631546213601 src/Tools/Code/code_thingol.ML --- a/src/Tools/Code/code_thingol.ML Tue Jul 21 14:08:58 2009 +0200 +++ b/src/Tools/Code/code_thingol.ML Tue Jul 21 17:02:18 2009 +0200 @@ -82,10 +82,10 @@ val read_const_exprs: theory -> string list -> string list * string list val consts_program: theory -> string list -> string list * (naming * program) val cached_program: theory -> naming * program - val eval_conv: theory -> (sort -> sort) + val eval_conv: theory -> (naming -> program -> ((string * sort) list * typscheme) * iterm -> string list -> cterm -> thm) -> cterm -> thm - val eval: theory -> (sort -> sort) -> ((term -> term) -> 'a -> 'a) + val eval: theory -> ((term -> term) -> 'a -> 'a) -> (naming -> program -> ((string * sort) list * typscheme) * iterm -> string list -> 'a) -> term -> 'a end; @@ -803,8 +803,8 @@ val vs'' = map (fn (v, _) => (v, (the o AList.lookup (op =) vs o prefix "'") v)) vs'; in evaluator naming program ((vs'', (vs', ty')), t') deps end; -fun eval_conv thy prep_sort = Code_Preproc.eval_conv thy prep_sort o base_evaluator thy; -fun eval thy prep_sort postproc = Code_Preproc.eval thy prep_sort postproc o base_evaluator thy; +fun eval_conv thy = Code_Preproc.eval_conv thy o base_evaluator thy; +fun eval thy postproc = Code_Preproc.eval thy postproc o base_evaluator thy; (** diagnostic commands **) diff -r 6da9c2a49fed -r 631546213601 src/Tools/nbe.ML --- a/src/Tools/nbe.ML Tue Jul 21 14:08:58 2009 +0200 +++ b/src/Tools/nbe.ML Tue Jul 21 17:02:18 2009 +0200 @@ -439,9 +439,6 @@ fun normalize thy naming program ((vs0, (vs, ty)), t) deps = let - fun subst_const f = map_aterms (fn t as Term.Const (c, ty) => Term.Const (f c, ty) - | t => t); - val resubst_triv_consts = subst_const (Code.resubst_alias thy); val ty' = typ_of_itype program vs0 ty; fun type_infer t = singleton (TypeInfer.infer_types (Syntax.pp_global thy) (Sign.tsig_of thy) I @@ -453,8 +450,8 @@ val string_of_term = setmp show_types true (Syntax.string_of_term_global thy); in compile_eval thy naming program (vs, t) deps + |> Code_Preproc.resubst_triv_consts thy |> tracing (fn t => "Normalized:\n" ^ string_of_term t) - |> resubst_triv_consts |> type_infer |> tracing (fn t => "Types inferred:\n" ^ string_of_term t) |> check_tvars @@ -463,9 +460,6 @@ (* evaluation oracle *) -fun add_triv_classes thy = curry (Sorts.inter_sort (Sign.classes_of thy)) - (Code.triv_classes thy); - fun mk_equals thy lhs raw_rhs = let val ty = Thm.typ_of (Thm.ctyp_of_term lhs); @@ -506,9 +500,9 @@ val norm_conv = no_frees_conv (fn ct => let val thy = Thm.theory_of_cterm ct; - in Code_Thingol.eval_conv thy (add_triv_classes thy) (norm_oracle thy) ct end); + in Code_Thingol.eval_conv thy (norm_oracle thy) ct end); -fun norm thy = no_frees_rew (Code_Thingol.eval thy (add_triv_classes thy) I (normalize thy)); +fun norm thy = no_frees_rew (Code_Thingol.eval thy I (normalize thy)); (* evaluation command *)