(* Subject: Mutually recursive rule induction *) (* Author: Myra Van Inwegen *) (* Part of the author's doctoral dissertation *) (* Summary: check_inductive_relations : term list -> (* patterns *) term -> (* term giving rules *) term list (* each term corresponds to a quantified rule *) define_inductive_relations : term list -> (* patterns *) term -> (* term giving rules *) thm * thm (* rules_satisfied theorem, induction theorem *) prove_inversion_theorems : thm -> (* rules_satisfied theorem *) thm -> (* induction theorem *) thm list (* inversion theorems *) prove_strong_induction : thm -> (* rules_satisfied theorem *) thm -> (* induction theorem *) thm (* strong induction theorem *) rule_induct : thm -> (* induction theorem (strong or regular) *) tactic (* sets up induction *) *) (* For interactive session, do the following: load "utilsLib"; *) structure ind_rel :> ind_rel = struct open HolKernel Parse boolLib; infix THEN THENL THENC ORELSE ORELSEC THEN_TCL ORELSE_TCL ## |->; infixr -->; val nth = List.nth; fun QCONV c tm = c tm handle _ => REFL tm; (* SUPPOSE_TAC : term -> tactic (term = t) [A] t1 ======================= [A,t] t1 [A] t *) local val bool = (==`:bool`==) in fun SUPPOSE_TAC new_claim current_goal = if type_of new_claim = bool then ([(new_claim::(fst current_goal),snd current_goal), (fst current_goal, new_claim)], fn [goalthm,claimthm] => MP (DISCH new_claim goalthm) claimthm | _ => raise HOL_ERR {origin_structure = "define_inductive_relations", origin_function = "SUPPOSE_TAC", message = "invalid application"}) else raise HOL_ERR {origin_structure = "define_inductive_relations", origin_function = "SUPPOSE_TAC", message = "The claim doesn't have type :bool"} end (* ADD_STRIP_ASSUMS_THEN : {new_assumptions:term list, tactic:tactic} -> tactic Like ADD_ASSUMS_THEN except it strips the new assumptions before adding them to the assumptions. *) fun ADD_STRIP_ASSUMS_THEN {new_assumptions = [], tactic} (asms,goal) = tactic (asms,goal) | ADD_STRIP_ASSUMS_THEN {new_assumptions = (claim::rest), tactic} (asms,goal) = if exists (aconv claim) asms then ADD_STRIP_ASSUMS_THEN {new_assumptions = rest, tactic = tactic} (asms,goal) else (SUPPOSE_TAC claim THENL [((POP_ASSUM STRIP_ASSUME_TAC) THEN (ADD_STRIP_ASSUMS_THEN {new_assumptions=rest,tactic=tactic})), ALL_TAC]) (asms,goal) (* use_thm : {theorem:thm, thm_tactic:(thm -> tactic)} -> tactic For adding the hypotheses of a theorem to the assumptions of a goal before applying the tactic resulting from applying thm_tactic to the given theorem. *) fun use_thm {theorem, thm_tactic} = ADD_STRIP_ASSUMS_THEN{new_assumptions = hyp theorem, tactic = thm_tactic theorem} (* from utilsLib.MP_IMP_TAC: MP_IMP_TAC : thm -> tactic ( thm = [A1] |- t2 ==> t1 ) [A] t1 ========== [A] t2 *) fun MP_IMP_TAC imp_thm (thisgoal as (asms,goal)) = if is_imp (concl imp_thm) then if aconv (snd (dest_imp (concl imp_thm))) goal then use_thm {theorem = imp_thm, thm_tactic = fn imp_thm => fn (asms,goal) => ([(asms,fst(dest_imp(concl imp_thm)))], fn [thm] => MP imp_thm thm | _ => raise HOL_ERR {origin_structure = "define_inductive_relations", origin_function = "MP_IMP_TAC", message = "invalid application"})} thisgoal else raise HOL_ERR {origin_structure = "define_inductive_relations", origin_function = "MP_IMP_TAC", message = "theorem doesn't imply goal"} else raise HOL_ERR {origin_structure = "define_inductive_relations", origin_function = "MP_IMP_TAC", message = "theorem is not an implication"} (* This function takes in the rules, checks them, quantifies them, and returns the quantified term to the user to look over and make sure it makes sense. Error messages are printed out if there are problems. Errors are reported according to rule number, where the first rule is rule 0. In other words, if there's a message complaining about an error in rule n, then that bad rule is nth (strip_conj rules_term, n). *) fun check_inductive_relations patterns rules_term = let fun member item (thing::more_things) = if item = thing then true else member item more_things | member item [] = false (* if neither A_list nor B_list have any duplicates, but possibly A_list and B_list have some common elements, then the result will be a list with no common elements *) fun append_no_dup (A_list, B_list) = let fun helper (A::As) B_list As_to_add = if member A B_list then helper As B_list As_to_add else helper As B_list (A::As_to_add) | helper [] B_list As_to_add = (rev As_to_add)@B_list in helper A_list B_list [] end (* val nth = Sml_system.List.nth *) (* if ftn_type is a1_ty -> a2_ty -> ... -> an_ty, this function returns the "argument" types, [a1_ty, a2_ty, ... a(n-1)_ty] *) fun get_arg_types ftn_type = let fun helper the_type arg_types = let val (tyop, args) = dest_type the_type in if (tyop = "fun") andalso (args <> []) then helper (nth (args, 1)) ((hd args)::arg_types) else rev arg_types end in helper ftn_type [] end (* This makes sure that a list of variables are different from some set of variables to avoid, as well as each other. Send in the list of vars you want to have distinct names as (var::vars), [] as new_vars, and the variables to avoid as vars_to_avoid *) fun ensure_vars_different (var::vars) new_vars vars_to_avoid = let val new_var = Term.variant vars_to_avoid var in ensure_vars_different vars (new_var::new_vars) (new_var::vars_to_avoid) end | ensure_vars_different [] new_vars _ = rev new_vars fun foldr ftn base (b::bs) = ftn (b, (foldr ftn base bs)) | foldr ftn base [] = base (* takes all existential variables in goal, and instantiates them to the same variable *) fun multi_var_exists (asm, gl) = let val (vars, tm) = strip_exists gl in foldr (fn (var, tac) => (EXISTS_TAC var) THEN tac) ALL_TAC vars (asm, gl) end; (* first goal -- break down the term and check it *) val (relations, vars_list) = foldr (fn (tm, (rels, vars)) => let val (rel, more_vars) = strip_comb tm in (rel::rels, (ensure_vars_different more_vars [] [])::vars) end) ([], []) patterns val orig_rules = strip_conj rules_term val all_variables = all_vars rules_term (* relations are variables at this point *) fun relations_in_tm tm = if is_var tm then member tm relations else if is_const tm then false else if is_abs tm then relations_in_tm (body tm) else (* must be comb *) let val (t1, t2) = dest_comb tm in relations_in_tm t1 orelse relations_in_tm t2 end (* this function makess sure that the rules are of the form needed *) fun check_rule rule_num rule = let fun check_hyp (hyp1::hyps) = let val (rator, rands) = strip_comb hyp1 in if member rator relations then (* check that the relations don't occur in rands *) if (foldr (fn (tm, acc) => relations_in_tm tm orelse acc) false rands) then raise HOL_ERR {message = "found relation being defined"^ " in arg to "^(fst(dest_var rator))^ " in hypothesis ofrule number "^ (Lib.int_to_string rule_num), origin_function = "check_rule", origin_structure = "define_inductive_relations"} else check_hyp hyps else if relations_in_tm hyp1 then raise HOL_ERR {message = "found relation being defined"^ " in side condition in rule number "^ (Lib.int_to_string rule_num), origin_function = "check_rule", origin_structure = "define_inductive_relations"} else check_hyp hyps end | check_hyp [] = true fun check_concl tm = let val (rator, rands) = strip_comb tm in if not (member rator relations) then raise HOL_ERR {message = "must have relation as operator in "^ "conclusion of rule "^(Lib.int_to_string rule_num), origin_function = "check_rule", origin_structure = "define_inductive_relations"} else if (foldr (fn (tm, acc) => relations_in_tm tm orelse acc) false rands) then raise HOL_ERR {message = "found relation being defined"^ " in arg to "^(fst(dest_var rator))^ " in conclusion of rule number "^ (Lib.int_to_string rule_num), origin_function = "check_rule", origin_structure = "define_inductive_relations"} else true end in if is_imp rule then let val (hyp1, conc) = dest_imp rule in check_hyp (strip_conj hyp1) andalso check_concl conc end else check_concl rule end fun check_rules rule_num (rule::rules) = check_rule rule_num rule andalso check_rules (rule_num + 1) rules | check_rules _ [] = true val _ = check_rules 0 orig_rules (* now sort the rules according to the relation that they are for *) fun rule_defines_relation rule relation = if is_imp rule then relation = fst (strip_comb (snd (dest_imp rule))) else relation = fst (strip_comb rule) val sorted_rules = map (fn rel => (filter (fn x => rule_defines_relation x rel) orig_rules)) relations (* put the rules back together into one list *) val rules = foldr (fn (l1, l2) => l1@l2) [] sorted_rules (* now quantify the rules -- that is, universally quantify vars in conclusion and existentially those in the hypothesis *) fun quantify_rule rule = if is_imp rule then let val (t1, t2) = dest_imp rule val vars_in_t2 = filter (fn v => not (member v relations)) (free_vars t2) val total_vars = vars_in_t2@relations val vars_in_t1 = filter (fn v => not (member v total_vars)) (free_vars t1) val new_t1 = list_mk_exists (rev vars_in_t1, t1) val new_imp = mk_imp (new_t1, t2) in list_mk_forall (rev vars_in_t2, new_imp) end else let val vars_in_rule = filter (fn v => not (member v relations)) (free_vars rule) in list_mk_forall (rev vars_in_rule, rule) end val new_rules = map quantify_rule rules in new_rules end (* Function define_inductive_relations patterns rules_term: term list -> term -> (thm * thm) Input: The patterns give, for each relation, a term of the form rel vars The purpose of this is twofold -- to give the order in which the user prefers to see the relations listed, and to give some nice variable names to use in the theorems. The goal is that rules_term specifies all the rules for defining relations rel_1 ... rel_n. The form of rules_term was chosen to be a compromise between being not too offensive for a user to type in, and being readable. So we do not require that the variables be quantified in the rules, since it clutters the specification. (However, this means that between the rules, the same variables must have the same types.) We also put all the rules together in one term to avoid having the users having to supply too much type information (the bigger the term, the more HOL type inference has to work with). Thus the form is: rule_0 /\ rule_1 /\ ... /\ rule_m Each rule_i (there is no particular order that the rules have to be in, but the theorem proved will have the rules sorted according to the relation they are defining) must be a rule for one of the relations, say rel_k, and must have either of the two following forms: (rel_k ) (an axiom) or ((hyp_1 /\ hyp_2 /\ ... /\ hyp_ni) ==> rel_k ) (rule with hypotheses) where each hyp_j has the form rel_m or side_condition (an arbitrary boolean, does not involve rel_1 ... rel_n) Each rule_i actually represents: (!. rel_k ) or (!. (?. hyp_1 /\ hyp_2 /\ ... /\ hyp_ni) ==> rel_k ) where = non-relation vars free in hyp_1, hyp_2, ... hyp_ni that are not free in the conclusion. ------------ Output: Two theorems are returned as a pair, (thm1, thm2). The first is a conjunction, where each conjunct says that the new relations satisfy one rule. The second is the induction theorem for the new relations. I made an attempt to give pretty good error messages. Errors are reported according to rule number, where the first rule is rule 0. In other words, if there's a message complaining about an error in rule n, then that bad rule is nth (strip_conj rules_term, n). *) fun define_inductive_relations patterns rules_term = let fun member item (thing::more_things) = if item = thing then true else member item more_things | member item [] = false (* if neither A_list nor B_list have any duplicates, but possibly A_list and B_list have some common elements, then the result will be a list with no common elements *) fun append_no_dup (A_list, B_list) = let fun helper (A::As) B_list As_to_add = if member A B_list then helper As B_list As_to_add else helper As B_list (A::As_to_add) | helper [] B_list As_to_add = (rev As_to_add)@B_list in helper A_list B_list [] end (* val nth = Sml_system.List.nth *) (* if ftn_type is a1_ty -> a2_ty -> ... -> an_ty, this function returns the "argument" types, [a1_ty, a2_ty, ... a(n-1)_ty] *) fun get_arg_types ftn_type = let fun helper the_type arg_types = let val (tyop, args) = dest_type the_type in if (tyop = "fun") andalso (args <> []) then helper (nth (args, 1)) ((hd args)::arg_types) else rev arg_types end in helper ftn_type [] end (* This makes sure that a list of variables are different from some set of variables to avoid, as well as each other. Send in the list of vars you want to have distinct names as (var::vars), [] as new_vars, and the variables to avoid as vars_to_avoid *) fun ensure_vars_different (var::vars) new_vars vars_to_avoid = let val new_var = Term.variant vars_to_avoid var in ensure_vars_different vars (new_var::new_vars) (new_var::vars_to_avoid) end | ensure_vars_different [] new_vars _ = rev new_vars fun foldr ftn base (b::bs) = ftn (b, (foldr ftn base bs)) | foldr ftn base [] = base (* takes all existential variables in goal, and instantiates them to the same variable *) fun multi_var_exists (asm, gl) = let val (vars, tm) = strip_exists gl in foldr (fn (var, tac) => (EXISTS_TAC var) THEN tac) ALL_TAC vars (asm, gl) end; (* first goal -- break down the term and check it *) val (relations, vars_list) = foldr (fn (tm, (rels, vars)) => let val (rel, more_vars) = strip_comb tm in (rel::rels, (ensure_vars_different more_vars [] [])::vars) end) ([], []) patterns val orig_rules = strip_conj rules_term val all_variables = all_vars rules_term (* relations are variables at this point *) fun relations_in_tm tm = if is_var tm then member tm relations else if is_const tm then false else if is_abs tm then relations_in_tm (body tm) else (* must be comb *) let val (t1, t2) = dest_comb tm in relations_in_tm t1 orelse relations_in_tm t2 end (* this function makess sure that the rules are of the form needed *) fun check_rule rule_num rule = let fun check_hyp (hyp1::hyps) = let val (rator, rands) = strip_comb hyp1 in if member rator relations then (* check that the relations don't occur in rands *) if (foldr (fn (tm, acc) => relations_in_tm tm orelse acc) false rands) then raise HOL_ERR {message = "found relation being defined"^ " in arg to "^(fst(dest_var rator))^ " in hypothesis ofrule number "^ (Lib.int_to_string rule_num), origin_function = "check_rule", origin_structure = "define_inductive_relations"} else check_hyp hyps else if relations_in_tm hyp1 then raise HOL_ERR {message = "found relation being defined"^ " in side condition in rule number "^ (Lib.int_to_string rule_num), origin_function = "check_rule", origin_structure = "define_inductive_relations"} else check_hyp hyps end | check_hyp [] = true fun check_concl tm = let val (rator, rands) = strip_comb tm in if not (member rator relations) then raise HOL_ERR {message = "must have relation as operator in "^ "conclusion of rule "^(Lib.int_to_string rule_num), origin_function = "check_rule", origin_structure = "define_inductive_relations"} else if (foldr (fn (tm, acc) => relations_in_tm tm orelse acc) false rands) then raise HOL_ERR {message = "found relation being defined"^ " in arg to "^(fst(dest_var rator))^ " in conclusion of rule number "^ (Lib.int_to_string rule_num), origin_function = "check_rule", origin_structure = "define_inductive_relations"} else true end in if is_imp rule then let val (hyp1, conc) = dest_imp rule in check_hyp (strip_conj hyp1) andalso check_concl conc end else check_concl rule end fun check_rules rule_num (rule::rules) = check_rule rule_num rule andalso check_rules (rule_num + 1) rules | check_rules _ [] = true val _ = check_rules 0 orig_rules (* now sort the rules according to the relation that they are for *) fun rule_defines_relation rule relation = if is_imp rule then relation = fst (strip_comb (snd (dest_imp rule))) else relation = fst (strip_comb rule) val sorted_rules = map (fn rel => (filter (fn x => rule_defines_relation x rel) orig_rules)) relations (* put the rules back together into one list *) val rules = foldr (fn (l1, l2) => l1@l2) [] sorted_rules (* now quantify the rules -- that is, universally quantify vars in conclusion and existentially those in the hypothesis *) fun quantify_rule rule = if is_imp rule then let val (t1, t2) = dest_imp rule val vars_in_t2 = filter (fn v => not (member v relations)) (free_vars t2) val total_vars = vars_in_t2@relations val vars_in_t1 = filter (fn v => not (member v total_vars)) (free_vars t1) val new_t1 = list_mk_exists (rev vars_in_t1, t1) val new_imp = mk_imp (new_t1, t2) in list_mk_forall (rev vars_in_t2, new_imp) end else let val vars_in_rule = filter (fn v => not (member v relations)) (free_vars rule) in list_mk_forall (rev vars_in_rule, rule) end val new_rules = map quantify_rule rules val num_rules = length new_rules (* now put together the terms that we need to define the relations *) val predicate = list_mk_abs (relations, list_mk_conj new_rules) fun add_poss var = let val (n, t) = dest_var var in mk_var ("poss_"^n, t) end val poss_relations = ensure_vars_different (map add_poss relations) [] all_variables val applied_pred = list_mk_comb (predicate, poss_relations) val vars_to_avoid = poss_relations@all_variables fun define_relations (vars::more_vars) (reltn::more_reltns) (poss_rel::more_poss) = let val applied_poss = list_mk_comb (poss_rel, vars) val impli = mk_imp (applied_pred, applied_poss) val quant = list_mk_forall (poss_relations, impli) val applied_reltn = list_mk_comb (reltn, vars) val def = mk_eq (applied_reltn, quant) in (new_definition ((fst (dest_var reltn))^"_DEF", def)):: (define_relations more_vars more_reltns more_poss) end | define_relations _ _ _ = [] (* define all the relations *) val the_definitions = define_relations vars_list relations poss_relations (* the next goal is to prove that relations we've defined satisfy the rules *) (* these are the constants we've defined *) val relatn_consts = map (mk_const o dest_var) relations (* The idea with the following three functions is that I use information in the rule corresponding to this goal to tell me how I ought to solve the goal. The count parameters keeps track of what rule we're currently operating on, so I can just grab the appropriate assumption and ASSUME it rather than using FIRST_ASSUM to find it for me. This idea is that it ought to go somewhat faster that way. *) fun mk_more_tactics num_hyps count (hyp1::hyps) = let val (rator, rands) = strip_comb hyp1 fun mk_still_more_tactics count = if count < num_rules + num_hyps then (fn (asms, gl) => let val rule_thm = ASSUME (nth (rev asms, count)) in (ACCEPT_TAC rule_thm) (asms, gl) end)::mk_still_more_tactics (count + 1) else [] (* new_rules have vars for relations *) val is_sentence = member rator relations val yet_more_tactics = if is_sentence then mk_still_more_tactics num_hyps else [] in fn (asms, gl) => let val rule_thm = ASSUME (nth (rev asms, count)) in if is_sentence then (MP_IMP_TAC (SPEC_ALL rule_thm) THEN REPEAT CONJ_TAC THENL yet_more_tactics) (asms, gl) else (ACCEPT_TAC rule_thm) (asms, gl) end end::mk_more_tactics num_hyps (count + 1) hyps | mk_more_tactics _ _ [] = [] fun mk_tactics count (rule::rules) = let val (forall_vars, body_tm) = strip_forall rule val is_an_imp = is_imp body_tm val hyp1 = if is_an_imp then fst (dest_imp body_tm) else --`T`-- val (exists_vars, hyp2) = if is_an_imp then strip_exists hyp1 else ([], --`T`--) val hyps = if is_an_imp then strip_conj hyp2 else [] val hyp_count = length hyps val more_tactics = if is_an_imp then mk_more_tactics hyp_count 0 hyps else [] in if ((not is_an_imp) andalso (forall_vars = [])) then (mk_tactics (count + 1) rules) else (fn (asms, gl) => let val rule_thm = ASSUME (nth (rev asms, hyp_count + count)) in if is_an_imp then (MP_IMP_TAC (SPEC_ALL rule_thm) THEN multi_var_exists THEN REPEAT CONJ_TAC THENL more_tactics) (asms, gl) else ACCEPT_TAC (SPEC_ALL rule_thm) (asms, gl) end)::(mk_tactics (count + 1) rules) end | mk_tactics _ [] = [] val tactics = mk_tactics 0 new_rules (* do the proof that the relations so defined do indeed satisfy the rules *) val first_rules_sat = TAC_PROOF (([], list_mk_comb (predicate, relatn_consts)), BETA_TAC THEN REPEAT CONJ_TAC THEN PURE_REWRITE_TAC the_definitions THEN BETA_TAC THEN REPEAT STRIP_TAC THENL tactics) val rules_sat = BETA_RULE first_rules_sat (* the next goal is to define and prove the induction theorem *) fun mk_prop_vars count (rel::rels) = mk_var ("P_"^(Lib.int_to_string count), snd (dest_var rel)) :: mk_prop_vars (count + 1) rels | mk_prop_vars _ [] = [] val all_arg_vars = foldr (fn (vars, more_vars) => append_no_dup (vars, more_vars)) [] vars_list val prop_vars = ensure_vars_different (mk_prop_vars 0 relations) [] all_arg_vars fun mk_conjuncts (vars::more_vars) (con::more_cons) (prop_var::more_props) = let val impl = mk_imp (list_mk_comb (con, vars), list_mk_comb (prop_var, vars)) val quantified = list_mk_forall (vars, impl) in quantified::(mk_conjuncts more_vars more_cons more_props) end | mk_conjuncts _ _ _ = [] val conjuncts = list_mk_conj (mk_conjuncts vars_list relatn_consts prop_vars) val applied_pred2 = list_mk_comb (predicate, prop_vars) val induction_thm_term = list_mk_forall (prop_vars, mk_imp (applied_pred2, conjuncts)) fun finish_tac (asms, gl) = let val thm1 = SPECL prop_vars (ASSUME (hd asms)) val thm2 = ASSUME (nth (asms, 1)) in (MP_IMP_TAC thm1 THEN ACCEPT_TAC thm2) (asms, gl) end val ind_thm1 = TAC_PROOF (([], induction_thm_term), BETA_TAC THEN PURE_REWRITE_TAC the_definitions THEN BETA_TAC THEN REPEAT GEN_TAC THEN DISCH_TAC THEN REPEAT CONJ_TAC THEN REPEAT GEN_TAC THEN DISCH_TAC THEN finish_tac) val ind_thm2 = BETA_RULE ind_thm1 in (rules_sat, ind_thm2) end (* prove_inversion_theorems proves the "case analysis" or "inversion" theorems for a given set of rules defining mutually recursive inductive relations. Basically, given the two theorems returned by define_inductive_relations (that is, the theorems stating that the relations satisfy the rules and the induction theorem, in that order), it returns a list of theorems, one for each relation. These theorems have the form: |- !. rel = where in the big disjunction, there is one disjunct for each rule pertaining to the relation rel. The form of each disjunct is ?evars. (var1 = term1) /\ ... /\ (varn = termn) /\ hyp where each vari is one of the argvars, and each termi consists of constants and vars from evars, and hyp is the hypothesis of the rule. Well, actually, the hypothesis of the rule actually has the form (? vars. t1 /\ ... /\ tk) In the disjunct, the vars will be among the evars, and hyp will be just t1 /\ ... /\ tk. *) fun prove_inversion_theorems rules_sat ind_thm = let (* Based strongly on Tom Melham's package, as translated by Konrad Slind. The complicated-looking comments are grabbed verbatim from that code. *) (* --------------------------------------------------------------------- *) (* |- ~~P *) (* -------- NOT_NOT *) (* |- P *) (* --------------------------------------------------------------------- *) fun NOT_NOT th = CCONTR (dest_neg(dest_neg (concl th))) (UNDISCH th); fun LIST_EXISTS_THEN f th = let val (vs,body) = strip_exists(concl th) val th1 = DISCH body (f (ASSUME body)) in MP (itlist EXISTS_IMP vs th1) th end; fun RULE thm1 thm2 = let val (xs,imp) = strip_exists (concl thm1) val thm = SPECL xs thm2 val impth = MP (ASSUME imp) thm val iimp = DISCH imp impth in MATCH_MP (itlist EXISTS_IMP xs iimp) thm1 end; (* --------------------------------------------------------------------- *) (* EXISTS_IMP2 : existentially quantify the antecedent and conclusion *) (* of an implication. *) (* *) (* A |- P ==> Q *) (* -------------------------- EXISTS_IMP "x" *) (* A |- (?x.P) ==> (?x.Q) *) (* *) (* LIKE built-in, but doesn't quantify in Q if not free there. *) (* Actually, used only in context where x not free in Q. *) (* *) (* --------------------------------------------------------------------- *) fun EXISTS_IMP2 x th = let val (ant,conseq) = dest_imp(concl th) in if (free_in x conseq) then let val th1 = EXISTS (mk_exists(x,conseq),x) (UNDISCH th) val asm = mk_exists(x,ant) in DISCH asm (CHOOSE (x,ASSUME asm) th1) end else let val asm = mk_exists(x,ant) in DISCH asm (CHOOSE (x,ASSUME asm) (UNDISCH th)) end end; fun efn v th = if (free_in v (concl th)) then EXISTS(mk_exists(v,concl th),v) th else th; fun mk_new_subst L2 L1 = map2 (fn rdx => fn rsd => {redex=rdx,residue=rsd}) L1 L2; fun RULE2 vs thm1 thm2 = let val (xs,P) = strip_exists(concl thm1) val (ys,Q) = strip_exists(concl thm2) fun itfn v vs = let val v' = Term.variant (vs @ xs) v in (v'::vs) end val ys' = itlist itfn ys [] val Q' = subst(mk_new_subst ys' ys) Q val asm = CONJ (ASSUME P) (ASSUME Q) val cs = LIST_CONJ (CONJUNCTS asm) val vs = filter (C free_in (concl cs)) (xs @ ys') val eth = MP (itlist EXISTS_IMP2 xs (DISCH P (itlist efn vs cs))) thm1 val ethh = MP (itlist EXISTS_IMP2 ys' (DISCH Q' eth)) thm2 in ethh end; (* ---------------------------------------------------------------------*) (* INTERNAL FUNCTION : LIST_NOT_FORALL *) (* *) (* If: *) (* |- ~P *) (* --------------- f : thm->thm *) (* |- Q |- R *) (* *) (* Then: *) (* *) (* |- ~!x1 ... xi. P *) (* ---------------------------- *) (* |- ?x1 ... xi. Q |- R *) (* ---------------------------------------------------------------------*) local fun efn v th = EXISTS(mk_exists(v,concl th),v) th in fun LIST_NOT_FORALL f th = let val (vs,body1) = strip_forall (dest_neg (concl th)) in if (null vs) then f th else let val (Q,R) = f (ASSUME(mk_neg body1)) val nott = itlist efn vs Q val thm = CCONTR body1 (MP (ASSUME (mk_neg (concl nott))) nott) in (CCONTR (concl nott) (MP th (GENL vs thm)), R) end end end; local fun chfn v (a,th) = let val tm = mk_exists(v,a) in (tm,CHOOSE (v,ASSUME tm) th) end in fun simp_axiom sfn vs ax th = let (* imp has form ~~(rel args ==> eqtns) |- rel args ==> eqtns *) val imp = NOT_NOT th (* ant = rel args, conseq = eqtns *) val (ant,conseq) = dest_imp (concl imp) val eqs = strip_conj conseq (* avs = forall_vars, res = rel args *) val (avs,res) = strip_forall (concl ax) val this_rel = fst (strip_comb res) (* inst is |- rel *) val inst = INST (fst(match_term res ant)) (SPECL avs ax) (* ths is ~~(rel args ==> eqtns) |- eqtns *) val ths = MP imp inst (* thm is eqtns |- rel *) val thm = sfn (ASSUME(concl ths)) this_rel inst (* rthm is |- (?. eqtns) ==> rel *) val rth = (uncurry DISCH) (itlist chfn vs ((concl ths),thm)) in (ths,rth) end end; (* relations are constants *) fun rel_in_term rel tm = if is_var tm then false else if is_const tm then rel = tm else if is_abs tm then rel_in_term rel (body tm) else (* must be comb *) let val (t1, t2) = dest_comb tm in (rel_in_term rel t1) orelse (rel_in_term rel t2) end fun foldr ftn base (b::bs) = ftn (b, (foldr ftn base bs)) | foldr ftn base [] = base (* The form of tm is (?exists_vars. t1 /\ ... /\ tn), where some of the ti have the form ~(rel args ==> some_term). This function proves: (?exists_vars. t1 /\ ... /\ tn) |- (?exists_vars. t1' /\ ... /\ tn') where if ti has form ~(rel args ==> some_term), then ti' has form (rel args), OW ti' = ti *) local fun mk_1_imp rel hyp = if not (rel_in_term rel hyp) then ASSUME hyp else CONJUNCT1 (PURE_REWRITE_RULE [NOT_IMP] (ASSUME hyp)) in fun mk_implication rel tm = let val (term_exists_vars, tm2) = strip_exists tm val term_conjs = strip_conj tm2 (* imp_thms says, for each i, ti |- ti' *) val imp_thms = map (mk_1_imp rel) term_conjs (* imp_thm has form [t1, ... , tn] |- t1' /\ ... /\ tn' *) val imp_thm = LIST_CONJ imp_thms (* need to get thm of form t1 /\ ... /\ tn |- t1' /\ ... /\ tn' -- this is imp_thm2 *) val imp_thm2 = foldr (fn (thm1, thm2) => PROVE_HYP thm1 thm2) imp_thm (CONJUNCTS (ASSUME tm2)) in (* now existentially quantify over the variables in hyp and concl *) UNDISCH (foldr (fn (var, thm) => EXISTS_IMP var thm) (DISCH_ALL imp_thm2) term_exists_vars) end end local val rule = NOT_NOT o CONV_RULE(RAND_CONV LIST_BETA_CONV) fun chfn v (a,th) = let val tm = mk_exists(v,a) in (tm,CHOOSE (v,ASSUME tm) th) end and efn v th = EXISTS(mk_exists(v,concl th),v) th in fun simp_rule sfn set vs rul th = let (* c1 = antecedant of term, c2 = conseq of term where term is roughly the conclusion of th, is term corresponding with rul *) val (c1,c2) = CONJ_PAIR (CONV_RULE (REWR_CONV NOT_IMP) th) (* th1 is rel ==> eqtns *) val th1 = NOT_NOT c2 val imp = concl th1 (* gvs is forall_vars in rule, cnc is rel *) val (gvs,cnc) = (I ## rand) (strip_forall(concl rul)) (* th3 = |- *) val th3 = UNDISCH (SPECL gvs rul) (* pat is rel *) val pat = fst(dest_imp imp) val this_rel = fst (strip_comb pat) (* change conjuncts of form ~(rel args ==> eqtns) to (rel args) *) val th2 = if (rel_in_term this_rel (concl c1)) then PROVE_HYP c1 (mk_implication this_rel (concl c1)) else c1 (* inst is substitution that replaces rule vars with vars from term *) val inst = fst(match_term (concl th3) pat) (* th_a is rule with vars from term instead of original vars *) val th_a = INST inst (DISCH_ALL th3) (* rins is term |- *) (* The line below used to use MATCH_MP, not MP. I can't see how th_a could be universally quantified, and it caused a bug by MATCH_MP sticking primes on things where they didn't belong, so it's now just MP. If there's a problem here, this may need to be looked into more closely *) val rins = MP th_a th2 (* erins is |- *) (* MP below used to be MATCH_MP, see note above *) val erins = MP th_a (ASSUME (concl th2)) (* eqns is term |- eqtns *) val eqns = RULE th1 rins (* eths is eqtn terms *) val eths = strip_conj (concl eqns) (* thm is [eqtns, ] |- rel *) val thm = sfn (LIST_CONJ (map ASSUME eths)) this_rel erins (* vv is existential vars in hypothesis, cs = conjs in hypothesis *) val (vv,cs) = (I ## strip_conj) (strip_exists(concl th2)) (* thx is same as thm, except with conjs in broken up *) val thx = PROVE_HYP (itlist efn vv (LIST_CONJ (map ASSUME cs))) thm (* simp_thm = term |- ?exists_vars. eqtns /\ hpy *) val simp_thm = RULE2 vs eqns th2 (* nevs, cn are exists_vars, big_conj of simp_thm *) val (nevs,cn) = strip_exists(concl simp_thm) val hys = CONJUNCTS (ASSUME cn) val (hh,nthm) = itlist chfn nevs (cn,itlist PROVE_HYP hys thx) val res = (uncurry DISCH) (itlist chfn vs (hh,nthm)) in (PROVE_HYP th simp_thm, res) end end; fun bad_error ftn_name = raise HOL_ERR {message = "this case should never happen, real problem here!", origin_function = ftn_name, origin_structure = "prove_inversion_theorems"} fun simp set sfn rul th = let val vs = fst(strip_forall (dest_neg (concl th))) val rule_body = snd (strip_forall (concl rul)) in if is_imp rule_body then LIST_NOT_FORALL (simp_rule sfn set vs rul) th else LIST_NOT_FORALL (simp_axiom sfn vs rul) th end; fun last [a] = a | last (_::rst) = last rst | last [] = bad_error "last" fun butlast [_] = [] | butlast (h::t) = h::(butlast t) | butlast [] = bad_error "butlast" local val thms = CONJUNCTS (SPEC_ALL AND_CLAUSES) in val T_and_clauses = GEN_ALL (CONJ (hd thms) (hd (tl thms))) end exception mymap2_ERR; fun mymap2 ([],[]) = [] | mymap2 ([],_) = raise mymap2_ERR | mymap2 (_,[]) = raise mymap2_ERR | mymap2 ((h1::rst1),(h2::rst2)) = mk_eq(h1,h2)::mymap2(rst1,rst2); fun divide_by_numbers (0::nums) elts partial_list full_lists = divide_by_numbers nums elts [] ((rev partial_list)::full_lists) | divide_by_numbers (num::nums) (elt::more_elts) partial_list full_lists = divide_by_numbers ((num-1)::nums) more_elts (elt::partial_list) full_lists | divide_by_numbers _ _ _ full_lists = rev full_lists local val v1 = genvar(==`:bool`==) and v2 = genvar(==`:bool`==) val thm = fst(EQ_IMP_RULE(CONJUNCT1 (SPECL [v1,v2] DE_MORGAN_THM))) fun IDISJ th1 th2 = let val di = mk_disj(rand(rator(concl th1)), rand(rator(concl th2))) in DISCH di (DISJ_CASES (ASSUME di) (UNDISCH th1) (UNDISCH th2)) end fun ITDISJ th1 th2 = let val (hy1,cl1) = dest_thm th1 and (hy2,cl2) = dest_thm th2 val _ = if not(length hy1 = 1) then raise Match else () val _ = if not(length hy2 = 1) then raise Match else () val dth = UNDISCH (INST [{redex=v1,residue=rand (hd hy1)}, {redex=v2,residue=rand (hd hy2)}] thm) in DISJ_CASES_UNION dth th1 th2 end in fun LIST_DE_MORGAN f rules fthm = let val conjs2 = strip_conj (dest_neg (concl fthm)) val (ts1,ts2) = split (map2 (fn r => fn t => f r (ASSUME(mk_neg t))) rules conjs2) in (PROVE_HYP fthm (end_itlist ITDISJ ts1), end_itlist IDISJ ts2) end end (* val nth = List.nth *) fun DISCH_nth n thm1 = let val asms = fst (dest_thm thm1) in DISCH (nth (asms, n)) thm1 end fun elim_nth n (item::items) = if (n = 0) then items else item::(elim_nth (n - 1) items) | elim_nth n _ = [] (* the goal here is to prove |- tm = T. I have |- rule so the goal is to prove |- rule ==> tm, then get |- tm, then |- tm = T *) fun process_rule rel tm rule = (* the form of tm is !forall_vars. (?exists_vars. hyp1 /\ ... /\ hypn) ==> some_rel args the form of rule is |- !forall_vars. (?exists_vars. hyp1' /\ ... /\ hypn') ==> some_rel args where for side conditions and hyps not involving rel, hypi = hypi', but for others, hypi = ~(rel argvars ==> (conjunction of equations)) and hypi' = rel argvars. *) let val (forall_vars, term_body) = strip_forall tm val speced_rule = SPECL forall_vars rule val (term_ant, term_conseq) = dest_imp term_body (* imp_thm3 says (?exists_vars. hyp1 /\ ... /\ hypn) |- (?exists_vars. hyp1' /\ ... /\ hypn') *) val imp_thm3 = mk_implication rel term_ant (* imp_thm4 says |- (?exists_vars. hyp1 /\ ... /\ hypn) ==> some_rel args *) val imp_thm4 = DISCH_ALL (MP speced_rule imp_thm3) (* now quantify over the forall_vars *) val proved_term = GENL forall_vars imp_thm4 (* now introduce T to get |- tm = T *) in EQT_INTRO proved_term end (* process_term is geven a term and a rule, and is expected to return a theorem saying |- tm = T *) fun process_term rel tm rule = let val (forall_vars, rule_body) = strip_forall (concl rule) in if not (is_imp rule_body) orelse not (rel_in_term rel tm) then EQT_INTRO rule else process_rule rel tm rule end (* assemble a list of props such that only the one referring to this relation is something other than the relation itslef *) fun assemble_preds count (pred::more_preds) (rel::more_rels) = if count = 0 then pred::(assemble_preds (count - 1) more_preds more_rels) else rel::(assemble_preds (count - 1) more_preds more_rels) | assemble_preds count _ _ = [] fun subst_in_subst theta = map (fn {redex,residue} => {redex=redex, residue = subst theta residue}); (* --------------------------------------------------------------------- *) (* INTERNAL FUNCTION : reduce *) (* *) (* A call to *) (* *) (* reduce [v1;...;vn] ths [] [] *) (* *) (* reduces the list of theorems ths to an equivalent list by removing *) (* theorems of the form |- vi = ti where vi does not occur free in ti, *) (* first using this equation to substitute ti for vi in all the other *) (* theorems. The theorems in ths are processed sequentially, so for *) (* example: *) (* *) (* reduce [a;b] [|- a=1; |- b=a+2; |- c=a+b] [] [] *) (* *) (* is reduced in the following stages: *) (* *) (* [|- a=1; |- b=a+2; |- c=a+b] *) (* *) (* ===> [|- b=1+2; |- c=1+b] (by the substitution [1/a]) *) (* ===> [|- c=1+(1+2)] (by the substitution [1+2/b]) *) (* *) (* The function returns the reduced list of theorems, paired with a list *) (* of the substitutions that were made, in reverse order. The result *) (* for the above example would be [|- c = 1+(1+2)],[("1+2",b);("1",a)]. *) (* --------------------------------------------------------------------- *) fun reduce vs ths res subf = if (null ths) then (rev res, subf) else let val (lhs,rhs) = dest_eq(concl(hd ths)) val (sth,pai) = if (mem lhs vs) then (hd ths,{redex=lhs,residue=rhs}) else if (mem rhs vs) then (SYM(hd ths),{redex=rhs,residue=lhs}) else bad_error ("reduce") in if (free_in (#redex pai) (#residue pai)) then bad_error ("reduce") else let val sfn = map (SUBS [sth]) val ssfn = subst_in_subst [pai] in reduce vs (sfn (tl ths)) (sfn res) (pai::ssfn subf) end end handle _ => reduce vs (tl ths) (hd ths::res) subf fun subst_assoc tm = let fun assc [] = NONE | assc ({redex,residue}::rst) = if (tm = redex) then (SOME residue) else assc rst in assc end; (* --------------------------------------------------------------------- *) (* REDUCE : simplify an existentially quantified conjuction by *) (* eliminating conjuncts of the form |- v=t, where v is among the *) (* quantified variables and v does not appear free in t. For example *) (* suppose: *) (* *) (* tm = "?vi. ?vs. C1 /\ ... /\ v = t /\ ... /\ Cn" *) (* *) (* then the result is: *) (* *) (* |- (?vi. ?vs. C1 /\ ... /\ vi = ti /\ ... /\ Cn) *) (* = *) (* (?vs. C1[ti/vi] /\ ... /\ Cn[ti/vi]) *) (* *) (* The equations vi = ti can appear as ti = vi, and all eliminable *) (* equations are eliminated. Fails unless there is at least one *) (* eliminable equation. Also flattens conjuncts. Reduces term to "T" if *) (* all variables eliminable. *) (* ---------------------------------------------------------------------*) local fun chfn v (a,th) = let val tm = mk_exists(v,a) val th' = if (free_in v (concl th)) then EXISTS (mk_exists(v,concl th),v) th else th in (tm,CHOOSE (v,ASSUME tm) th') end fun efn ss v (pat,th) = let val wit = case (subst_assoc v ss) of NONE => v | (SOME residue) => residue val ex = mk_exists(v,pat) val epat = subst ss ex in (ex,EXISTS(epat,wit) th) end fun prove ths cs = (uncurry CONJ ((prove ths ## prove ths) (dest_conj cs))) handle _ => (Lib.first (fn t => concl t = cs) ths) handle _ => (REFL (rand cs)) in fun REDUCE tm = let val (vs,cs) = strip_exists tm val (remn,ss) = reduce vs (CONJUNCTS (ASSUME cs)) [] [] in if (null ss) then bad_error ("REDUCE") else let val th1 = LIST_CONJ remn handle _ => TRUTH val th2 = (uncurry DISCH) (itlist chfn vs (cs,th1)) val (rvs,rcs) = strip_exists(rand(concl th2)) val eqt = subst ss cs val th3 = prove (CONJUNCTS (ASSUME rcs)) eqt val (_,th4) = itlist (efn ss) vs (cs,th3) val th5 = (uncurry DISCH) (itlist chfn rvs (rcs,th4)) in IMP_ANTISYM_RULE th2 th5 end end end; (* Here the computations begin *) val rule_thms = CONJUNCTS rules_sat (* the first goal is to come up with terms representing the properties that we want. *) (* props is variables for properties *) val (props, tm1) = strip_forall (concl ind_thm) (* ind_ant says properties satisfy rules, ind_conseq say that, for each relation, !. rel ==> P *) val (ind_ant, ind_conseq) = dest_imp tm1 (* collect together the argvars -- the vars the relations are applied to in the conclusion of the induction thm *) val (argvars, imps) = foldr (fn (tm, (vars, imps)) => let val (more_vars, an_imp) = strip_forall tm in (more_vars::vars, an_imp::imps) end) ([], []) (strip_conj ind_conseq) (* now name them differently, so we have no clashes among var names, also name them to be different from the existentially quantified vars in the rules *) val exists_vars = foldr (fn (tm, vars) => let val b1 = snd (strip_forall tm) val not_axiom = is_imp b1 val more_vars = if not_axiom then fst (strip_exists (fst (dest_imp b1))) else [] in if not_axiom then more_vars@vars else vars end) [] (map concl rule_thms) fun rename_vars (vars::more_vars) vars_to_avoid renamed_vars = let fun do_one_bunch_vars (var::more_var) used_vars new_vars = let val tmp_var = Term.variant used_vars var in do_one_bunch_vars more_var (tmp_var::used_vars) (tmp_var::new_vars) end | do_one_bunch_vars _ _ new_vars = rev new_vars val new_vars = do_one_bunch_vars vars vars_to_avoid [] in rename_vars more_vars (new_vars@vars_to_avoid) (new_vars::renamed_vars) end | rename_vars [] _ renamed_vars = rev renamed_vars val renamed_argvars = rename_vars argvars exists_vars [] (* replace the vars in imps with renamed vars each item in new_imps has form: rel = prop argvars *) fun modify_imps (old_vars::more_old) (new_vars::more_new) (imp::more_imps) = (subst (mk_new_subst new_vars old_vars) imp):: modify_imps more_old more_new more_imps | modify_imps _ _ _ = [] val new_imps = modify_imps argvars renamed_argvars imps (* info_list is an association list with, for each relation, the argvars and hypothesis (which is rel ) *) val info_list = map2 (fn vars => fn imp => let val hyp = rand (rator imp) val rel = fst (strip_comb hyp) in (rel, (vars, hyp)) end) renamed_argvars new_imps (* sfn is used to substitute vars used in rules for vars used in terms in conclusion of thm4 below *) fun sfn eqs rel = let val (argvars, hyp) = assoc rel info_list in (* following line changed by PVH Feb 3, 2000 from {var=v, thm=th} *) SUBST(map2 (fn th => fn v => {redex=v, residue=th}) (map SYM (CONJUNCTS eqs)) argvars) hyp end (* list of relations *) val set = map fst info_list (* divide up the rules according to which relation it's for *) fun has_this_rel rel thm1 = let val bdy = snd (strip_forall (concl thm1)) val applied_rel = if is_imp bdy then snd (dest_imp bdy) else bdy in rel = fst (strip_comb applied_rel) end val divided_rules = map (fn rel => (filter (fn thm1 => has_this_rel rel thm1) rule_thms)) set (* specialize ind_thm to prop vars *) val tmp_thm1 = UNDISCH (SPECL props ind_thm) (* imp_thms = theorems saying rel ==> prop *) val imp_thms = map2 (fn vars => fn theorem => SPECL vars theorem) renamed_argvars (CONJUNCTS tmp_thm1) (* speced_ind = induction with foralls for props and argvars removed *) val speced_ind = DISCH_nth 0 (foldr (fn (thm1, thm2) => CONJ thm1 thm2) (last imp_thms) (butlast imp_thms)) (* find number of rules for each relation *) val rules_count = map length divided_rules (* genvars contains, for each var in renamed_argvars, a corresponding genvar *) val genvars = map (fn vars => map (genvar o type_of) vars) renamed_argvars (* make the predicates. there is one for each relation, it looks like \. ~(rel ==> (argvar_1 = genvar_1) /\ ... /\ (argvar_n = genvar_n)) *) fun mk_preds (gen_vars::more_gens) (arg_vars::more_args) (thm1::more_thms) = let val eqtns = list_mk_conj (mymap2 (arg_vars, gen_vars)) val theta = map2 (fn r1 => fn r2 => {redex=r1,residue=r2}) arg_vars gen_vars val assum = subst theta (rator (concl thm1)) val pred = list_mk_abs (gen_vars, mk_neg (mk_comb (assum, eqtns))) in pred::(mk_preds more_gens more_args more_thms) end | mk_preds _ _ _ = [] val preds = mk_preds genvars renamed_argvars imp_thms val hyps = map (rand o rator) new_imps fun mk_inversion_thms count all_rels (hyp::hyps) (vars::more_vars) = let val new_preds = assemble_preds count preds all_rels val rel = nth (all_rels, count) val theta = map2 (fn prop_var => fn pred => {redex = prop_var, residue = pred}) props new_preds (* replace P_0, P_1, etc, with the predicates *) val thm1 = INST theta speced_ind (* get the "preds satisfy rules" term *) val preds_sat_rules = fst (dest_imp (concl thm1)) (* basically, eliminate unwanted conclusions, and put "preds satisfy rules" and "rel argvars" into hypotheses *) val thm2 = BETA_RULE (UNDISCH (nth (CONJUNCTS (UNDISCH thm1), count))) (* make the theorem that is contradictory to thm2 *) val contr = DISCH hyp (ADD_ASSUM hyp (LIST_CONJ (map REFL vars))) (* now do contradiction, getting ~"preds satisfy rules" in conclusion *) val thm3 = BETA_RULE (NOT_INTRO (DISCH preds_sat_rules (MP thm2 contr))) (* thm3 has form ~(conj1 /\ ... /\ conjn) where each conj corresponds to one rule -- need to eliminate conjs that correspond to rules that don't apply to this relation *) (* grab the conjuncts that don't correspond to this relation *) val divided_conjs = divide_by_numbers rules_count (strip_conj (dest_neg (concl thm3))) [] [] (* these are the conjs that we need to get rid of, and the rules that correspond with them *) val conjs = flatten (elim_nth count divided_conjs) val rules = flatten (elim_nth count divided_rules) (* get the theorems that say |- conji = T *) val rewrites = map2 (process_term rel) conjs rules (* rewrite with the |- conji = T and get rid of T conjuncts, so now thm4 says ~(predicates satisfy rules), but the conjuncts corresponding to rules for other relations have been eliminated *) val thm4 = PURE_REWRITE_RULE (T_and_clauses::rewrites) thm3 (* get the rules pertaining to this relation *) val relevant_rules = nth (divided_rules, count) (* now do Tom-like munging to get process info to get it in the correct form *) (* a_thm = assuming rel , case disjunctions are true, b_thm = case disjunctions ==> rel *) val (a_thm, b_thm) = LIST_DE_MORGAN (simp set sfn) relevant_rules thm4 (* thm5 = rel = case disjunctions *) val thm5 = IMP_ANTISYM_RULE (DISCH_ALL a_thm) b_thm (* ds is a list of thms, each one says (disj for rule) = (simplified disj for rule) *) val ds = map (QCONV (TRY_CONV REDUCE)) (strip_disj(rand(concl thm5))) (* red has form (original distunctions) = (simplified disjunctions) *) val red = end_itlist (fn t1 => fn t2 => MK_COMB (AP_TERM (--`$\/`--) t1, t2)) ds (* the preceeding line changed from `\/` to `$\/` for Taupo-4 by PVH, October 19, 2000 *) (* final result is that !. rel = (case disjunctions) *) in (GENL vars (TRANS thm5 red)):: (mk_inversion_thms (count + 1) all_rels hyps more_vars) end | mk_inversion_thms _ _ _ _ = [] in mk_inversion_thms 0 set hyps renamed_argvars (* fun mk_inversion_thms count all_rels (hyp::hyps) (vars::more_vars) = *) end (* The usual induction theorem states: to prove that !. rel_1 ==> P_1 /\ ... ** !. rel_n ==> P_n you need to show that the properties P_0 thru P_n satisfy the rules. (Note that since the relations were defined as the smallest relations that satisfy the rules, this implies that if some tuple is in our relations, then it satisfies any other set of relations that satisfy the rules.) Each rule looks like this: !. (?. hyp_1 /\ hyp_2 /\ ... /\ hyp_m) ==> rel_k [constants and ] where each hyp_i can be either a side condition (not mentioning any of the relations) or a hypothesis involving one of the relations, that is, be something like rel_p [constants and and ] Let us say that a rule is: !. (?. SC_1 /\ rel_1 /\ rel_3 /\ SC_2) ==> rel_2 Thus to show **, you'll need to prove !. (?. SC_1 /\ P_1 /\ P_3 /\ SC_2) ==> P_2 The strong induction theorem says that to prove ** you can show that the relations satisfy the rules, with the additional hypotheses that the relations hold of the args. That is, for our hypothetical rule, you'll need to show that: !. (?. SC_1 /\ P_1 /\ rel_1 /\ P_3 rel_3 /\ /\ SC_2) ==> P_2 This is theoretically equivalent to the original induction principle, in fact it's easily proven from the original and the fact that the relations satisfy the rules. The strong induction theorem does, however, come in handy if you need some fact about the relation to show that the properties satisfy the rules. *) fun prove_strong_induction rules_sat ind_thm = let val (prop_vars, ind_imp) = strip_forall (concl ind_thm) val conseq_conjs = strip_conj (snd (dest_imp ind_imp)) val vars_relation_list = map (fn tm => let val (vars, tm2) = strip_forall tm in (vars, fst (strip_comb (fst (dest_imp tm2)))) end) conseq_conjs val relations = map snd vars_relation_list fun mk_new_prop prop_var (vars, reltn) = let val conj = mk_conj (list_mk_comb (prop_var, vars), list_mk_comb (reltn, vars)) in list_mk_abs (vars, conj) end val new_props = map2 mk_new_prop prop_vars vars_relation_list val new_thm = BETA_RULE (SPECL new_props ind_thm) (* now we have: modified rules ==> modified concl. We need to eliminate unwanted conjuncts from the modified rules and modified concl. I'll do the latter first: a conjunct in the concl looks like: !. reltn ==> prop_var /\ reltn I want it to look like !. reltn ==> prop_var I'll show that the second implies the first *) val (mod_rules, mod_concl) = dest_imp (concl new_thm) fun conjunct_n n th = if not (is_conj (concl th)) then th else if n = 0 then CONJUNCT1 th else conjunct_n (n - 1) (CONJUNCT2 th) val and_thm = GEN_ALL (conjunct_n 4 (SPEC_ALL AND_CLAUSES)) fun do_one_conjunct tm = let val (vars, bod) = strip_forall tm val rel_tm = fst (dest_imp bod) val thm1 = CONJUNCT1 (UNDISCH (SPEC_ALL (ASSUME tm))) in DISCH_ALL (GENL vars (DISCH rel_tm thm1)) end fun prove_conj_imp (tm::tms) = if tms = [] then do_one_conjunct tm else let val thm1 = do_one_conjunct tm val thm2 = prove_conj_imp tms in IMP_CONJ thm1 thm2 end | prove_conj_imp [] = REFL (--`T`--) (* so SML doesn't complain *) val concl_thm = prove_conj_imp (strip_conj mod_concl) (* now to remove unwanted conjuncts from the modified rules. A conjunct term here looks like: !. mod_hyp1 /\ mod_hyp2 /\ ... mod_hypn ==> prop_var /\ reltn where each mod_hypi is a side condition, or has form: prop_var /\ reltn what I want is to show that this conjunct term is implied by !. (flattened hypotheses) ==> prop_var where by flattened hypotheses I mean that the () are removed from the mod_hypi's that are not side conditions. *) (* delete the conjs that don't satisfy pred *) local val DISJ_IMP_THM = GSYM IMP_DISJ_THM val DISJ_IMP_THM1 = REWRITE_RULE[NOT_CLAUSES] (GEN (--`A:bool`--)(SPEC (--`~(A:bool)`--) DISJ_IMP_THM)) fun delete_conjs1 pred conj_thm = let fun helper conj_thm so_far = if is_cond (concl conj_thm) then let val cd_thm = CONV_RULE (REWR_CONV COND_EXPAND) conj_thm val (disj1,disj2) = CONJ_PAIR cd_thm val imp1 = CONV_RULE (REWR_CONV DISJ_IMP_THM ) disj1 val imp2 = CONV_RULE (REWR_CONV DISJ_IMP_THM1) disj2 val body1 = UNDISCH imp1 val body2 = UNDISCH imp2 val res1 = delete_conjs1 pred body1 val res2 = delete_conjs1 pred body2 val rimp1 = DISCH (fst (dest_imp (concl imp1))) res1 val rimp2 = DISCH (fst (dest_imp (concl imp2))) res2 val rdisj1 = CONV_RULE (REWR_CONV IMP_DISJ_THM ) rimp1 val rdisj2 = CONV_RULE (REWR_CONV (GSYM DISJ_IMP_THM1)) rimp2 val rcd = CONJ rdisj1 rdisj2 val rconj_thm = CONV_RULE (REWR_CONV (GSYM COND_EXPAND)) rcd in rconj_thm::so_far end else if is_conj (concl conj_thm) then let val conj1 = CONJUNCT1 conj_thm in if is_cond (concl conj1) then helper (CONJUNCT2 conj_thm) ((helper conj1 [])@so_far) else if pred (concl conj1) then helper (CONJUNCT2 conj_thm) (conj1::so_far) else helper (CONJUNCT2 conj_thm) so_far end else if pred (concl conj_thm) then (conj_thm::so_far) else so_far in LIST_CONJ (rev (helper (REWRITE_RULE[GSYM CONJ_ASSOC] conj_thm) [])) end in fun delete_conjs pred conj_thm = DISCH_ALL (delete_conjs1 pred conj_thm) end (* Myra's original version, does not handle COND's as conjuncts: (* delete the conjs that don't satisfy pred *) fun delete_conjs pred conj_thm = let fun helper conj_thm so_far = if is_conj (concl conj_thm) then let val conj1 = CONJUNCT1 conj_thm in if pred (concl conj1) then helper (CONJUNCT2 conj_thm) (conj1::so_far) else helper (CONJUNCT2 conj_thm) so_far end else if pred (concl conj_thm) then (conj_thm::so_far) else so_far in DISCH_ALL (LIST_CONJ (rev (helper conj_thm []))) end *) fun member item (thing::more_things) = if item = thing then true else member item more_things | member item [] = false fun props_in_tm tm = if is_var tm then member tm prop_vars else if is_const tm then false else if is_abs tm then props_in_tm (body tm) else (* must be comb *) let val (t1, t2) = dest_comb tm in props_in_tm t1 orelse props_in_tm t2 end fun foldr ftn base (b::bs) = ftn (b, (foldr ftn base bs)) | foldr ftn base [] = base fun do_one_conj2 rule tm = let val (vars, bod) = strip_forall tm in if is_imp bod then let val (ex_mod_hyps, prop_and_rel) = dest_imp bod val prop_tm = fst (dest_conj prop_and_rel) val (exists_vars, mod_hyps) = strip_exists ex_mod_hyps val mod_hyp_list = strip_conj mod_hyps val new_mod_hyps = list_mk_conj mod_hyp_list val ex_new_mod_hyps = list_mk_exists (exists_vars, new_mod_hyps) val speced_rule = SPECL vars rule val thm1 = ASSUME (list_mk_forall (vars, mk_imp (ex_new_mod_hyps, prop_tm))) val thm2 = SPEC_ALL thm1 fun pred tm = not (props_in_tm tm) val conj_imp = delete_conjs pred (ASSUME new_mod_hyps) val ex_conj_imp = foldr (fn (var, thm) => EXISTS_IMP var thm) conj_imp exists_vars val conjs_imp_reltn = IMP_TRANS ex_conj_imp speced_rule val thm3 = PURE_ONCE_REWRITE_RULE [and_thm] (IMP_CONJ thm2 conjs_imp_reltn) val thm4 = PURE_ONCE_REWRITE_RULE [CONJUNCTS_CONV (new_mod_hyps, mod_hyps)] thm3 in DISCH_ALL (GENL vars thm4) end else let val (prop_tm, reltn_tm) = dest_conj bod val thm1 = ASSUME (list_mk_forall (vars, prop_tm)) val thm2 = GENL vars (CONJ (SPEC_ALL thm1) (SPECL vars rule)) in DISCH_ALL thm2 end end (* val ((rule, tm)::more_info) = more_info; val thm1 = do_one_conj2 rule tm *) fun prove_conj_imp2 ((rule, tm)::more_info) = if null more_info then do_one_conj2 rule tm else let val thm1 = do_one_conj2 rule tm val thm2 = prove_conj_imp2 more_info in IMP_CONJ thm1 thm2 end | prove_conj_imp2 [] = REFL (--`T`--) (* so SML doesn't complain *) (* fun prove_conj_imp2 (((rule, tm)::more_info) :(thm * term)list) = if more_info = ([]:(thm * term)list) then do_one_conj2 rule tm else let val thm1 = do_one_conj2 rule tm val thm2 = prove_conj_imp2 more_info in IMP_CONJ thm1 thm2 end | prove_conj_imp2 [] = REFL (--`T`--) (* so SML doesn't complain *) *) (* The following was added by PVH on Feb. 25, 2000. It repairs strip_conj, which breaks apart elements of a conjunction which are themselves conjunctions; we wish to only do this at the top level. *) fun careful_strip_conj tm = let val (h, t) = dest_conj tm in (h :: (careful_strip_conj t)) end handle _ => [tm] val rules_thm = prove_conj_imp2 (zip (CONJUNCTS rules_sat) (careful_strip_conj mod_rules)) val almost_final_thm = IMP_TRANS (IMP_TRANS rules_thm new_thm) concl_thm in GENL prop_vars almost_final_thm end (* When given a goal of the form: (!. rel_0 ==> prop_0[]) /\ ... (!. rel_n ==> prop_n[]) where the rel_i are the relations mentioned in the conclusion of the induct_thm (they don't need to be in the same order), rule_induct sets up the induction for you. Works for strong induction thms as well as regular ones. *) local fun get_reltn tm = fst (strip_comb (fst (dest_imp (snd (strip_forall tm))))) fun process_term tm = (fst (strip_comb (fst (dest_imp (snd (strip_forall tm))))), tm) fun get_correct_tm ((rel, tm)::more_info) rel2 = if rel = rel2 then tm else get_correct_tm more_info rel2 | get_correct_tm [] rel2 = raise HOL_ERR {origin_structure = "inductive_relations", origin_function = "rule_induct", message = "need term for relation "^(fst (dest_const rel2))} in fun rule_induct induct_thm (asms, gl) = let val reltns_goals_list = map process_term (strip_conj gl) val concl_list = strip_conj (snd (dest_imp (snd (strip_forall (concl induct_thm))))) val reltns_in_ind = map get_reltn concl_list (* look thru' the list for the clause that corresponds to it *) val sorted_goals = map (get_correct_tm reltns_goals_list) reltns_in_ind val props_list = map (fn tm => let val (vars, t2) = strip_forall tm val applied_prop = snd (dest_imp t2) in list_mk_abs (vars, applied_prop) end) sorted_goals val speced_ind = BETA_RULE (SPECL props_list induct_thm) in MP_IMP_TAC speced_ind (asms, gl) end end end; (* ind_rel *)