# HG changeset patch # User Christian Urban # Date 1236691246 0 # Node ID 3f617d7a2691917d09637559d39e82129220b0b0 # Parent 2319cff107f07bf7717cad9c8f1ffb6c05ed536c more work on simple_inductive diff -r 2319cff107f0 -r 3f617d7a2691 CookBook/Appendix.thy --- a/CookBook/Appendix.thy Sun Mar 08 20:53:00 2009 +0000 +++ b/CookBook/Appendix.thy Tue Mar 10 13:20:46 2009 +0000 @@ -18,6 +18,12 @@ user space type systems (in the form that already exists) unification and typing algorithms + + useful datastructures: + + discrimination nets + + association lists *} end diff -r 2319cff107f0 -r 3f617d7a2691 CookBook/Package/Ind_Code.thy --- a/CookBook/Package/Ind_Code.thy Sun Mar 08 20:53:00 2009 +0000 +++ b/CookBook/Package/Ind_Code.thy Tue Mar 10 13:20:46 2009 +0000 @@ -1,26 +1,178 @@ theory Ind_Code -imports "../Base" Simple_Inductive_Package +imports "../Base" Simple_Inductive_Package Ind_Prelims begin +section {* Code *} + +subsection {* Definitions *} + +text {* + If we give it a term and a constant name, it will define the + constant as the term. +*} + +ML{*fun make_defs ((binding, syn), trm) lthy = +let + val arg = ((binding, syn), (Attrib.empty_binding, trm)) + val ((_, (_ , thm)), lthy) = LocalTheory.define Thm.internalK arg lthy +in + (thm, lthy) +end*} + +text {* + Returns the definition and the local theory in which this definition has + been made. What is @{ML Thm.internalK}? +*} + +ML {*let + val lthy = TheoryTarget.init NONE @{theory} +in + make_defs ((Binding.name "MyTrue", NoSyn), @{term "True"}) lthy +end*} + +text {* + Why is the output of MyTrue blue? +*} + +text {* + Constructs the term for the definition: the main arguments are a predicate + and the types of the arguments, it also expects orules which are the + intro rules in the object logic; preds which are all predicates. returns the + term. +*} + +ML %linenosgray{*fun defs_aux lthy orules preds (pred, arg_types) = +let + fun mk_all x P = HOLogic.all_const (fastype_of x) $ lambda x P + + val fresh_args = + arg_types + |> map (pair "z") + |> Variable.variant_frees lthy orules + |> map Free +in + list_comb (pred, fresh_args) + |> fold_rev (curry HOLogic.mk_imp) orules + |> fold_rev mk_all preds + |> fold_rev lambda fresh_args +end*} + +text {* + The lines 5-9 produce fresh arguments with which the predicate can be applied. + For this it pairs every type with a string @{text [quotes] "z"} (Line 7); then + generates variants for all these strings (names) so that they are unique w.r.t.~to + the intro rules; in Line 9 it generates the corresponding variable terms for these + unique names. + + The unique free variables are applied to the predicate (Line 11); then + the intro rules are attached as preconditions (Line 12); in Line 13 we + quantify over all predicates; and in line 14 we just abstract over all + the (fresh) arguments of the predicate. +*} + text {* - What does the @{ML Thm.internalK} do, in the LocalTheory.define Thm.internalK? + The arguments of the main function for the definitions are + the intro rules; the predicates and their names, their syntax + annotations and the argument types of each predicate. It + returns a theorem list (the definitions) and a local + theory where the definitions are made +*} + +ML %linenosgray{*fun definitions rules preds prednames syns arg_typss lthy = +let + val thy = ProofContext.theory_of lthy + val orules = map (ObjectLogic.atomize_term thy) rules + val defs = map (defs_aux lthy orules preds) (preds ~~ arg_typss) +in + fold_map make_defs (prednames ~~ syns ~~ defs) lthy +end*} + +text {* + In line 4 we generate the intro rules in the object logic; for this we have to + obtain the theory behind the local theory (Line 3); with this we can + call @{ML defs_aux} to generate the terms for the left-hand sides. + The actual definitions are made in Line 7. +*} + +subsection {* Introduction Rules *} + +ML{*fun inst_spec ct = + Drule.instantiate' [SOME (ctyp_of_term ct)] [NONE, SOME ct] @{thm spec}*} + +text {* + Instantiates the @{text "x"} in @{thm spec[no_vars]} with a @{ML_type cterm}. +*} + +text {* + Instantiates universal qantifications in the premises +*} + +lemma "\x\<^isub>1 x\<^isub>2 x\<^isub>3. P (x\<^isub>1::nat) (x\<^isub>2::nat) (x\<^isub>3::nat) \ True" +apply (tactic {* EVERY' (map (dtac o inst_spec) + [@{cterm "y\<^isub>1::nat"},@{cterm "y\<^isub>2::nat"},@{cterm "y\<^isub>3::nat"}]) 1*}) +(*<*)oops(*>*) + +text {* + The tactic for proving the induction rules: *} +ML{*fun induction_tac defs prems insts = + EVERY1 [ObjectLogic.full_atomize_tac, + cut_facts_tac prems, + K (rewrite_goals_tac defs), + EVERY' (map (dtac o inst_spec) insts), + assume_tac]*} + +lemma + assumes asm: "even n" + shows "P 0 \ + (\m. Q m \ P (Suc m)) \ (\m. P m \ Q (Suc m)) \ P n" +apply(tactic {* induction_tac [@{thm even_def}, @{thm odd_def}] [@{thm asm}] + [@{cterm "P::nat\bool"}, @{cterm "Q::nat\bool"}] *}) +done + +ML %linenosgray{*fun inductions rules defs preds Tss lthy1 = +let + val Ps = replicate (length preds) "P" + val (newprednames, lthy2) = Variable.variant_fixes Ps lthy1 + + val thy = ProofContext.theory_of lthy2 + + val Tss' = map (fn Ts => Ts ---> HOLogic.boolT) Tss + val newpreds = map Free (newprednames ~~ Tss') + val cnewpreds = map (cterm_of thy) newpreds + val rules' = map (subst_free (preds ~~ newpreds)) rules + + fun prove_induction ((pred, newpred), Ts) = + let + val zs = replicate (length Ts) "z" + val (newargnames, lthy3) = Variable.variant_fixes zs lthy2; + val newargs = map Free (newargnames ~~ Ts) + + val prem = HOLogic.mk_Trueprop (list_comb (pred, newargs)) + val goal = Logic.list_implies + (rules', HOLogic.mk_Trueprop (list_comb (newpred, newargs))) + in + Goal.prove lthy3 [] [prem] goal + (fn {prems, ...} => induction_tac defs prems cnewpreds) + |> singleton (ProofContext.export lthy3 lthy1) + end +in + map prove_induction (preds ~~ newpreds ~~ Tss) +end*} + +ML {* Goal.prove *} +ML {* singleton *} +ML {* ProofContext.export *} text {* - @{ML_chunk [display,gray] definitions_aux} - @{ML_chunk [display,gray,linenos] definitions} - *} text {* - - @{ML_chunk [display,gray] induction_rules} + @{ML_chunk [display,gray] subproof1} -*} - -text {* + @{ML_chunk [display,gray] subproof2} @{ML_chunk [display,gray] intro_rules} diff -r 2319cff107f0 -r 3f617d7a2691 CookBook/Package/Simple_Inductive_Package.thy --- a/CookBook/Package/Simple_Inductive_Package.thy Sun Mar 08 20:53:00 2009 +0000 +++ b/CookBook/Package/Simple_Inductive_Package.thy Tue Mar 10 13:20:46 2009 +0000 @@ -1,8 +1,62 @@ theory Simple_Inductive_Package -imports Main -uses ("simple_inductive_package.ML") +imports Main "../Base" +uses "simple_inductive_package.ML" begin +(* +simple_inductive + trcl :: "('a \ 'a \ bool) \ 'a \ 'a \ bool" +where + base: "trcl R x x" +| step: "trcl R x y \ R y z \ trcl R x z" + +thm trcl_def +thm trcl.induct +thm trcl.intros + +simple_inductive + even and odd +where + even0: "even 0" +| evenS: "odd n \ even (Suc n)" +| oddS: "even n \ odd (Suc n)" + +thm even_def odd_def +thm even.induct odd.induct +thm even0 +thm evenS +thm oddS +thm even_odd.intros + +simple_inductive + accpart for r :: "'a \ 'a \ bool" +where + accpartI: "(\y. r y x \ accpart r y) \ accpart r x" + +thm accpart_def +thm accpart.induct +thm accpartI + +locale rel = + fixes r :: "'a \ 'a \ bool" + +simple_inductive (in rel) accpart' +where + accpartI': "\x. (\y. r y x \ accpart' y) \ accpart' x" + + +context rel +begin + thm accpartI' + thm accpart'.induct +end + +thm rel.accpartI' +thm rel.accpart'.induct + + +lemma "True" by simp +*) use_chunks "simple_inductive_package.ML" diff -r 2319cff107f0 -r 3f617d7a2691 CookBook/Package/simple_inductive_package.ML --- a/CookBook/Package/simple_inductive_package.ML Sun Mar 08 20:53:00 2009 +0000 +++ b/CookBook/Package/simple_inductive_package.ML Tue Mar 10 13:20:46 2009 +0000 @@ -18,107 +18,143 @@ structure SimpleInductivePackage: SIMPLE_INDUCTIVE_PACKAGE = struct -fun mk_all x P = HOLogic.all_const (fastype_of x) $ lambda x P - -(* @chunk definitions_aux *) -fun definitions_aux ((binding, syn), trm) lthy = +(* @chunk make_definitions *) +fun make_defs ((binding, syn), trm) lthy = let - val ((_, (_, thm)), lthy) = - LocalTheory.define Thm.internalK ((binding, syn), (Attrib.empty_binding, trm)) lthy + val arg = ((binding, syn), (Attrib.empty_binding, trm)) + val ((_, (_ , thm)), lthy) = LocalTheory.define Thm.internalK arg lthy in (thm, lthy) end (* @end *) +(* @chunk definitions_aux *) +fun defs_aux lthy orules preds params (pred, arg_types) = +let + fun mk_all x P = HOLogic.all_const (fastype_of x) $ lambda x P + + val fresh_args = + arg_types + |> map (pair "z") + |> Variable.variant_frees lthy orules + |> map Free +in + list_comb (pred, fresh_args) + |> fold_rev (curry HOLogic.mk_imp) orules + |> fold_rev mk_all preds + |> fold_rev lambda (params @ fresh_args) +end +(* @end *) + (* @chunk definitions *) -fun definitions params rules preds preds' Tss lthy = +fun definitions rules params preds prednames syns arg_typess lthy = let val thy = ProofContext.theory_of lthy - val rules' = map (ObjectLogic.atomize_term thy) rules + val orules = map (ObjectLogic.atomize_term thy) rules + val defs = + map (defs_aux lthy orules preds params) (preds ~~ arg_typess) in - fold_map (fn ((((R, _), syn), pred), Ts) => - let - val zs = map Free (Variable.variant_frees lthy rules' (map (pair "z") Ts)) - - val t0 = list_comb (pred, zs); - val t1 = fold_rev (curry HOLogic.mk_imp) rules' t0; - val t2 = fold_rev mk_all preds' t1; - val t3 = fold_rev lambda (params @ zs) t2; - in - definitions_aux ((R, syn), t3) - end) (preds ~~ preds' ~~ Tss) lthy + fold_map make_defs (prednames ~~ syns ~~ defs) lthy end (* @end *) fun inst_spec ct = Drule.instantiate' [SOME (ctyp_of_term ct)] [NONE, SOME ct] @{thm spec}; +(* @chunk induction_tac *) +fun induction_tac defs prems insts = + EVERY1 [ObjectLogic.full_atomize_tac, + cut_facts_tac prems, + K (rewrite_goals_tac defs), + EVERY' (map (dtac o inst_spec) insts), + assume_tac] +(* @end *) + +(* @chunk induction_rules *) +fun inductions rules defs parnames preds Tss lthy1 = +let + val (_, lthy2) = Variable.add_fixes parnames lthy1 + + val Ps = replicate (length preds) "P" + val (newprednames, lthy3) = Variable.variant_fixes Ps lthy2 + + val thy = ProofContext.theory_of lthy3 + + val Tss' = map (fn Ts => Ts ---> HOLogic.boolT) Tss + val newpreds = map Free (newprednames ~~ Tss') + val cnewpreds = map (cterm_of thy) newpreds + val rules' = map (subst_free (preds ~~ newpreds)) rules + + fun prove_induction ((pred, newpred), Ts) = + let + val (newargnames, lthy4) = + Variable.variant_fixes (replicate (length Ts) "z") lthy3; + val newargs = map Free (newargnames ~~ Ts) + + val prem = HOLogic.mk_Trueprop (list_comb (pred, newargs)) + val goal = Logic.list_implies + (rules', HOLogic.mk_Trueprop (list_comb (newpred, newargs))) + in + Goal.prove lthy4 [] [prem] goal + (fn {prems, ...} => induction_tac defs prems cnewpreds) + |> singleton (ProofContext.export lthy4 lthy1) + end +in + map prove_induction (preds ~~ newpreds ~~ Tss) +end +(* @end *) + val all_elims = fold (fn ct => fn th => th RS inst_spec ct); val imp_elims = fold (fn th => fn th' => [th', th] MRS @{thm mp}); -(* @chunk induction_rules *) -fun INDUCTION rules preds' Tss defs lthy1 lthy2 = -let - val (Pnames, lthy3) = Variable.variant_fixes (replicate (length preds') "P") lthy2; - val Ps = map (fn (s, Ts) => Free (s, Ts ---> HOLogic.boolT)) (Pnames ~~ Tss); - val cPs = map (cterm_of (ProofContext.theory_of lthy3)) Ps; - val rules'' = map (subst_free (preds' ~~ Ps)) rules; - - fun prove_indrule ((R, P), Ts) = +(* @chunk subproof1 *) +fun subproof2 prem params2 prems2 = + SUBPROOF (fn {prems, ...} => let - val (znames, lthy4) = Variable.variant_fixes (replicate (length Ts) "z") lthy3; - val zs = map Free (znames ~~ Ts) + val prem' = prems MRS prem; + val prem'' = + case prop_of prem' of + _ $ (Const (@{const_name All}, _) $ _) => + prem' |> all_elims params2 + |> imp_elims prems2 + | _ => prem'; + in + rtac prem'' 1 + end) +(* @end *) - val prem = HOLogic.mk_Trueprop (list_comb (R, zs)) - val goal = Logic.list_implies (rules'', HOLogic.mk_Trueprop (list_comb (P, zs))) +(* @chunk subproof2 *) +fun subproof1 rules preds i = + SUBPROOF (fn {params, prems, context = ctxt', ...} => + let + val (prems1, prems2) = chop (length prems - length rules) prems; + val (params1, params2) = chop (length params - length preds) params; in - Goal.prove lthy4 [] [prem] goal - (fn {prems, ...} => EVERY1 - ([ObjectLogic.full_atomize_tac, - cut_facts_tac prems, - K (rewrite_goals_tac defs)] @ - map (fn ct => dtac (inst_spec ct)) cPs @ - [assume_tac])) |> - singleton (ProofContext.export lthy4 lthy1) - end; -in - map prove_indrule (preds' ~~ Ps ~~ Tss) - end + rtac (ObjectLogic.rulify (all_elims params1 (nth prems2 i))) 1 + THEN + EVERY1 (map (fn prem => subproof2 prem params2 prems2 ctxt') prems1) + end) (* @end *) (* @chunk intro_rules *) -fun INTROS rules preds' defs lthy1 lthy2 = +fun INTROS rules parnames preds defs lthy1 = let - fun prove_intro (i, r) = - Goal.prove lthy2 [] [] r - (fn {prems, context = ctxt} => EVERY - [ObjectLogic.rulify_tac 1, - rewrite_goals_tac defs, - REPEAT (resolve_tac [@{thm allI},@{thm impI}] 1), - SUBPROOF (fn {params, prems, context = ctxt', ...} => - let - val (prems1, prems2) = chop (length prems - length rules) prems; - val (params1, params2) = chop (length params - length preds') params; - in - rtac (ObjectLogic.rulify (all_elims params1 (nth prems2 i))) 1 - THEN - EVERY1 (map (fn prem => - SUBPROOF (fn {prems = prems', concl, ...} => - let - - val prem' = prems' MRS prem; - val prem'' = case prop_of prem' of - _ $ (Const (@{const_name All}, _) $ _) => - prem' |> all_elims params2 - |> imp_elims prems2 - | _ => prem'; - in rtac prem'' 1 end) ctxt') prems1) - end) ctxt 1]) |> - singleton (ProofContext.export lthy2 lthy1) + val (_, lthy2) = Variable.add_fixes parnames lthy1 + + fun prove_intro (i, goal) = + Goal.prove lthy2 [] [] goal + (fn {context = ctxt, ...} => + EVERY1 + [ObjectLogic.rulify_tac, + K (rewrite_goals_tac defs), + REPEAT o (resolve_tac [@{thm allI},@{thm impI}]), + subproof1 rules preds i ctxt]) + |> singleton (ProofContext.export lthy2 lthy1) in map_index prove_intro rules end + (* @end *) (* @chunk add_inductive_i *) @@ -129,12 +165,15 @@ val Tss = map (binder_types o fastype_of) preds'; val (ass,rules) = split_list specs; - val (defs, lthy1) = definitions params' rules preds preds' Tss lthy - val (_, lthy2) = Variable.add_fixes (map (Binding.name_of o fst) params) lthy1; + val prednames = map (fst o fst) preds + val syns = map snd preds + val parnames = map (Binding.name_of o fst) params + + val (defs, lthy1) = definitions rules params' preds' prednames syns Tss lthy; - val inducts = INDUCTION rules preds' Tss defs lthy1 lthy2 - - val intros = INTROS rules preds' defs lthy1 lthy2 + val inducts = inductions rules defs parnames preds' Tss lthy1 + + val intros = INTROS rules parnames preds' defs lthy1 val mut_name = space_implode "_" (map (Binding.name_of o fst o fst) preds); val case_names = map (Binding.name_of o fst o fst) specs diff -r 2319cff107f0 -r 3f617d7a2691 cookbook.pdf Binary file cookbook.pdf has changed