# HG changeset patch # User wenzelm # Date 1132406462 -3600 # Node ID 744803a2d5a530f8c064b669390b9282ef0415ed # Parent c3caf13f621d594f151b7bf04ca58b57aa08f211 induct: CONJUNCTS for multiple goals; added coinduct method; tuned; diff -r c3caf13f621d -r 744803a2d5a5 src/Provers/induct_method.ML --- a/src/Provers/induct_method.ML Sat Nov 19 14:21:01 2005 +0100 +++ b/src/Provers/induct_method.ML Sat Nov 19 14:21:02 2005 +0100 @@ -21,9 +21,11 @@ sig val cases_tac: Proof.context -> bool -> term option list list -> thm option -> thm list -> int -> RuleCases.tactic - val fix_tac: Proof.context -> (string * typ) list -> int -> tactic + val fix_tac: (string * typ) list -> int -> tactic val induct_tac: Proof.context -> bool -> (string option * term) option list list -> - thm option -> (string * typ) list -> thm list -> int -> RuleCases.tactic + (string * typ) list list -> thm option -> thm list -> int -> RuleCases.tactic + val coinduct_tac: Proof.context -> bool -> term option list -> thm option -> + thm list -> int -> RuleCases.tactic val setup: (theory -> theory) list end; @@ -33,7 +35,9 @@ (** misc utils **) -(* align lists *) +(* lists *) + +fun nth_list xss i = nth xss i handle Subscript => []; fun align_left msg xs ys = let val m = length xs and n = length ys @@ -46,8 +50,9 @@ (* prep_inst *) -fun prep_inst align cert tune (tm, ts) = +fun prep_inst thy align tune (tm, ts) = let + val cert = Thm.cterm_of thy; fun prep_var (x, SOME t) = let val cx = cert x; @@ -68,11 +73,21 @@ end; -(* warn_open *) +(* trace_rules *) + +fun trace_rules _ kind [] = error ("Unable to figure out " ^ kind ^ " rule") + | trace_rules ctxt _ rules = Method.trace ctxt rules; + + +(* make_cases *) fun warn_open true = warning "Encountered open rule cases -- deprecated" | warn_open false = (); +fun make_cases is_open rule = + RuleCases.make (tap warn_open is_open) NONE (Thm.theory_of_thm rule, Thm.prop_of rule); + + (** cases method **) @@ -103,27 +118,24 @@ fun inst_rule r = if null insts then RuleCases.add r else (align_left "Rule has fewer premises than arguments given" (Thm.prems_of r) insts - |> (List.concat o map (prep_inst align_left cert I)) + |> (List.concat o map (prep_inst thy align_left I)) |> Drule.cterm_instantiate) r |> rpair (RuleCases.get r); val ruleq = (case opt_rule of - NONE => - let val rules = find_casesS ctxt facts @ find_casesT ctxt insts @ [Data.cases_default] in - Method.trace ctxt rules; - Seq.maps (Seq.try inst_rule) (Seq.of_list rules) - end - | SOME r => Seq.single (inst_rule r)); - val ruleq_cases = ruleq |> Seq.maps (fn (th, (cases, n)) => - Method.multi_resolves (Library.take (n, facts)) [th] - |> Seq.map (apsnd (rpair (Library.drop (n, facts))) o rpair cases)); - - fun make_cases rule = RuleCases.make (tap warn_open is_open) NONE (thy, Thm.prop_of rule); + SOME r => Seq.single (inst_rule r) + | NONE => + (find_casesS ctxt facts @ find_casesT ctxt insts @ [Data.cases_default]) + |> tap (trace_rules ctxt InductAttrib.casesN) + |> Seq.of_list |> Seq.maps (Seq.try inst_rule)) + |> Seq.maps (fn (th, (cases, n)) => + Method.multi_resolves (Library.take (n, facts)) [th] + |> Seq.map (apsnd (rpair (Library.drop (n, facts))) o rpair cases)); in fn i => fn st => - ruleq_cases |> Seq.maps (fn (rule, (cases, facts)) => - (Method.insert_tac facts THEN' Tactic.rtac rule) i st - |> Seq.map (rpair (make_cases rule cases))) + ruleq |> Seq.maps (fn (rule, (cases, more_facts)) => + (Method.insert_tac more_facts THEN' Tactic.rtac rule) i st + |> Seq.map (rpair (make_cases is_open rule cases))) end; val cases_meth = Method.METHOD_CASES o ((Seq.DETERM o HEADGOAL) oo @@ -141,28 +153,28 @@ val meta_spec = PureThy.get_thm Pure.thy (Name "meta_spec"); -fun meta_spec_tac ctxt (x, T) i st = SUBGOAL (fn (goal, _) => +fun meta_spec_tac (x, T) i st = SUBGOAL (fn (goal, _) => let val thy = Thm.theory_of_thm st; val cert = Thm.cterm_of thy; val certT = Thm.ctyp_of thy; val v = Free (x, T); - val _ = Term.exists_subterm (fn t => t aconv v) goal orelse - error ("No variable " ^ ProofContext.string_of_term ctxt v ^ " in subgoal"); - val P = Term.absfree (x, T, goal); - val rule = meta_spec - |> Drule.instantiate' [SOME (certT T)] [SOME (cert P), SOME (cert v)] - |> Thm.rename_params_rule ([x], 1); - in compose_tac (false, rule, 1) end i) i st; + in + if Term.exists_subterm (fn t => t aconv v) goal then + let + val P = Term.absfree (x, T, goal); + val rule = meta_spec + |> Drule.instantiate' [SOME (certT T)] [SOME (cert P), SOME (cert v)] + |> Thm.rename_params_rule ([x], 1); + in compose_tac (false, rule, 1) i end + else all_tac + end) i st; in -fun fix_tac ctxt fixes = - (case gen_duplicates (op =) fixes of - [] => EVERY' (map (meta_spec_tac ctxt) (rev fixes)) - | dups => error ("Duplicate specification of variable(s): " ^ - commas (map (ProofContext.string_of_term ctxt o Free) dups))); +fun fix_tac fixes = + EVERY' (map meta_spec_tac (rev (gen_distinct (op =) fixes))); end; @@ -246,6 +258,8 @@ (* divinate rule instantiation -- cannot handle pending goal parameters *) +local + fun dest_env thy (env as Envir.Envir {iTs, ...}) = let val cert = Thm.cterm_of thy; @@ -255,6 +269,8 @@ val xs = map2 (cert o Var) (map #1 pairs, map (#T o Thm.rep_cterm) ts); in (map (fn (xi, (S, T)) => (certT (TVar (xi, S)), certT T)) (Vartab.dest iTs), xs ~~ ts) end; +in + fun divinate_inst rule i st = let val {thy, maxidx, ...} = Thm.rep_thm st; @@ -276,6 +292,8 @@ end end handle Subscript => Seq.empty; +end; + (* special renaming of rule parameters *) @@ -306,6 +324,14 @@ | special_rename_params _ _ thm = thm; +(* rule_versions *) + +fun rule_versions rule = Seq.cons (rule, + (Seq.make (fn () => SOME (localize rule, Seq.empty))) + |> Seq.filter (not o curry Thm.eq_thm rule)) + |> Seq.map (rpair (RuleCases.get rule)); + + (* induct_tac *) (* @@ -319,7 +345,7 @@ fun find_inductT ctxt insts = fold_rev multiply (insts |> List.mapPartial (fn [] => NONE | ts => List.last ts) - |> map (InductAttrib.find_inductT ctxt o fastype_of)) [[]] + |> map (InductAttrib.find_inductT ctxt o Term.fastype_of)) [[]] |> map join_rules |> List.concat; fun find_inductS ctxt (fact :: _) = InductAttrib.find_inductS ctxt fact @@ -327,56 +353,106 @@ in -fun induct_tac ctxt is_open def_insts opt_rule fixes facts = +fun induct_tac ctxt is_open def_insts fixes opt_rule facts = let val thy = ProofContext.theory_of ctxt; val cert = Thm.cterm_of thy; val ((insts, defs), defs_ctxt) = fold_map add_defs def_insts ctxt |>> split_list; - fun rule_versions r = Seq.cons (r, Seq.filter (not o curry Thm.eq_thm r) - (Seq.make (fn () => SOME (localize r, Seq.empty)))) - |> Seq.map (rpair (RuleCases.get r)); - val inst_rule = apfst (fn r => if null insts then r else (align_right "Rule has fewer conclusions than arguments given" (Data.dest_concls (Thm.concl_of r)) insts - |> (List.concat o map (prep_inst align_right cert (atomize_term thy))) + |> (List.concat o map (prep_inst thy align_right (atomize_term thy))) |> Drule.cterm_instantiate) r); val ruleq = (case opt_rule of - NONE => - let val rules = find_inductS ctxt facts @ - map (special_rename_params defs_ctxt insts) (find_inductT ctxt insts) - in - conditional (null rules) (fn () => error "Unable to figure out induct rule"); - Method.trace ctxt rules; - rules |> Seq.of_list |> Seq.maps rule_versions |> Seq.maps (Seq.try inst_rule) - end - | SOME r => r |> rule_versions |> Seq.map inst_rule); - val ruleq_cases = ruleq |> Seq.maps (fn (th, (cases, n)) => - Method.multi_resolves (Library.take (n, facts)) [th] - |> Seq.map (rpair (cases, n - length facts, Library.drop (n, facts)))); + SOME r => r |> rule_versions |> Seq.map inst_rule + | NONE => + (find_inductS ctxt facts @ + map (special_rename_params defs_ctxt insts) (find_inductT ctxt insts)) + |> tap (trace_rules ctxt InductAttrib.inductN) + |> Seq.of_list |> Seq.maps rule_versions |> Seq.maps (Seq.try inst_rule)) + |> Seq.maps (fn (th, (cases, n)) => + Method.multi_resolves (Library.take (n, facts)) [th] + |> Seq.map (rpair (cases, n - length facts, Library.drop (n, facts)))); - fun make_cases rule = + fun rule_cases rule = RuleCases.make (tap warn_open is_open) (SOME (Thm.prop_of rule)) (rulified_term rule); in - (fn i => fn st => ruleq_cases |> Seq.maps (fn (rule, (cases, k, more_facts)) => - (Method.insert_tac (List.concat defs @ more_facts) (* FIXME CONJUNCTS *) - THEN' fix_tac defs_ctxt fixes - THEN' atomize_tac) i st |> Seq.maps (fn st' => - divinate_inst (internalize k rule) i st' |> Seq.maps (fn rule' => - Tactic.rtac rule' i st' - |> Seq.maps (ProofContext.exports defs_ctxt ctxt) - |> Seq.map (rpair (make_cases rule' cases)))))) + (fn i => fn st => + ruleq |> Seq.maps (fn (rule, (cases, k, more_facts)) => + (CONJUNCTS (ALLGOALS (fn j => + Method.insert_tac (more_facts @ nth_list defs (j - 1)) j + THEN fix_tac (nth_list fixes (j - 1)) j)) + THEN' atomize_tac) i st |> Seq.maps (fn st' => + divinate_inst (internalize k rule) i st' |> Seq.maps (fn rule' => + Tactic.rtac rule' i st' + |> Seq.maps (ProofContext.exports defs_ctxt ctxt) + |> Seq.map (rpair (rule_cases rule' cases)))))) THEN_ALL_NEW_CASES rulify_tac end; val induct_meth = Method.RAW_METHOD_CASES o ((Seq.DETERM o HEADGOAL) oo - (fn (ctxt, (is_open, (insts, (opt_rule, fixes)))) => - induct_tac ctxt is_open insts opt_rule fixes)); + (fn (ctxt, (is_open, (insts, (fixes, opt_rule)))) => + induct_tac ctxt is_open insts fixes opt_rule)); + +end; + + + +(** coinduct method **) + +(* + rule selection scheme: + `x:A` coinduct ... - set coinduction + coinduct x - type coinduction + ... coinduct ... r - explicit rule +*) + +local + +fun find_coinductT ctxt (SOME t :: _) = InductAttrib.find_coinductT ctxt (Term.fastype_of t) + | find_coinductT _ _ = []; + +fun find_coinductS ctxt (fact :: _) = InductAttrib.find_coinductS ctxt fact + | find_coinductS _ _ = []; + +in + +fun coinduct_tac ctxt is_open inst opt_rule facts = + let + val thy = ProofContext.theory_of ctxt; + val cert = Thm.cterm_of thy; + + val inst_rule = apfst (fn r => + if null inst then r + else Drule.cterm_instantiate (prep_inst thy align_left I (Thm.concl_of r, inst)) r); + + val ruleq = + (case opt_rule of + SOME r => r |> rule_versions |> Seq.map inst_rule + | NONE => + (find_coinductS ctxt facts @ find_coinductT ctxt inst) + |> tap (trace_rules ctxt InductAttrib.coinductN) + |> Seq.of_list |> Seq.maps rule_versions |> Seq.maps (Seq.try inst_rule)) + |> Seq.maps (fn (th, (cases, n)) => + Method.multi_resolves (Library.take (n, facts)) [th] + |> Seq.map (apsnd (rpair (Library.drop (n, facts))) o rpair cases)); + in + fn i => fn st => + ruleq |> Seq.maps (fn (rule, (cases, more_facts)) => + (Method.insert_tac more_facts THEN' Tactic.rtac rule) i st |> Seq.maps (fn st' => + divinate_inst rule i st' |> Seq.maps (fn rule' => + Tactic.rtac rule' i st' + |> Seq.map (rpair (make_cases is_open rule' cases))))) + end; + +val coinduct_meth = Method.RAW_METHOD_CASES o ((Seq.DETERM o HEADGOAL) oo + (fn (ctxt, (is_open, (insts, opt_rule))) => + coinduct_tac ctxt is_open insts opt_rule)); end; @@ -385,9 +461,8 @@ (** concrete syntax **) val openN = "open"; +val fixingN = "fixing"; val ruleN = "rule"; -val ofN = "of"; -val fixingN = "fixing"; local @@ -403,6 +478,7 @@ val cases_rule = rule InductAttrib.lookup_casesT InductAttrib.lookup_casesS; val induct_rule = rule InductAttrib.lookup_inductT InductAttrib.lookup_inductS; +val coinduct_rule = rule InductAttrib.lookup_coinductT InductAttrib.lookup_coinductS; val inst = Scan.lift (Args.$$$ "_") >> K NONE || Args.local_term >> SOME; @@ -413,11 +489,13 @@ val free = Scan.state -- Args.local_term >> (fn (_, Free v) => v | (ctxt, t) => error ("Bad free variable: " ^ ProofContext.string_of_term ctxt t)); -val fixing = Scan.optional (Scan.lift (Args.$$$ fixingN -- Args.colon) |-- Scan.repeat1 free) []; fun unless_more_args scan = Scan.unless (Scan.lift - ((Args.$$$ InductAttrib.typeN || Args.$$$ InductAttrib.setN || Args.$$$ ruleN || - Args.$$$ ofN || Args.$$$ fixingN) -- Args.colon)) scan; + ((Args.$$$ fixingN || Args.$$$ InductAttrib.typeN || Args.$$$ InductAttrib.setN || + Args.$$$ ruleN) -- Args.colon)) scan; + +val fixing = Scan.optional (Scan.lift (Args.$$$ fixingN -- Args.colon) |-- + Args.and_list1 (Scan.repeat (unless_more_args free))) []; in @@ -426,7 +504,10 @@ val induct_args = Method.syntax (Args.mode openN -- (Args.and_list (Scan.repeat (unless_more_args def_inst)) -- - (Scan.option induct_rule -- fixing))); + (fixing -- Scan.option induct_rule))); + +val coinduct_args = Method.syntax (Args.mode openN -- + (Scan.repeat (unless_more_args inst) -- Scan.option coinduct_rule)); end; @@ -437,6 +518,7 @@ val setup = [Method.add_methods [(InductAttrib.casesN, cases_meth oo cases_args, "case analysis on types or sets"), - (InductAttrib.inductN, induct_meth oo induct_args, "induction on types or sets")]]; + (InductAttrib.inductN, induct_meth oo induct_args, "induction on types or sets"), + (InductAttrib.coinductN, coinduct_meth oo coinduct_args, "coinduction on types or sets")]]; end;