--- a/src/HOL/Subst/Unify.ML Wed May 21 10:09:21 1997 +0200
+++ b/src/HOL/Subst/Unify.ML Wed May 21 10:53:02 1997 +0200
@@ -1,4 +1,5 @@
(* Title: Subst/Unify
+ ID: $Id$
Author: Konrad Slind, Cambridge University Computer Laboratory
Copyright 1997 University of Cambridge
@@ -39,41 +40,27 @@
*---------------------------------------------------------------------------*)
Tfl.tgoalw Unify.thy [] unify.rules;
(* Wellfoundedness of unifyRel *)
-by (simp_tac (!simpset addsimps [unifyRel_def, uterm_less_def,
+by (simp_tac (!simpset addsimps [unifyRel_def,
wf_inv_image, wf_lex_prod, wf_finite_psubset,
wf_rel_prod, wf_measure]) 1);
(* TC *)
by (Step_tac 1);
by (simp_tac (!simpset addsimps [finite_psubset_def, finite_vars_of,
- lex_prod_def, measure_def,
- inv_image_def]) 1);
+ lex_prod_def, measure_def, inv_image_def]) 1);
by (rtac (monotone_vars_of RS (subset_iff_psubset_eq RS iffD1) RS disjE) 1);
by (Blast_tac 1);
-by (asm_simp_tac (!simpset addsimps [rprod_def, less_eq, less_add_Suc1]) 1);
+by (asm_simp_tac (!simpset addsimps [less_eq, less_add_Suc1]) 1);
qed "tc0";
(*---------------------------------------------------------------------------
- * Eliminate tc0 from the recursion equations and the induction theorem.
- *---------------------------------------------------------------------------*)
-val [wfr,tc] = Prim.Rules.CONJUNCTS tc0;
-val unifyRules0 = map (normalize_thm [fn th => wfr RS th, fn th => tc RS th])
- unify.rules;
-
-val unifyInduct0 = [wfr,tc] MRS unify.induct
- |> read_instantiate [("P","split Q")]
- |> rewrite_rule [split RS eq_reflection]
- |> standard;
-
-
-(*---------------------------------------------------------------------------
* Termination proof.
*---------------------------------------------------------------------------*)
-goalw Unify.thy [unifyRel_def,uterm_less_def,measure_def] "trans unifyRel";
+goalw Unify.thy [unifyRel_def, measure_def] "trans unifyRel";
by (REPEAT (resolve_tac [trans_inv_image, trans_lex_prod,
trans_finite_psubset, trans_less_than,
- trans_rprod, trans_inv_image] 1));
+ trans_inv_image] 1));
qed "trans_unifyRel";
@@ -85,7 +72,7 @@
goalw Unify.thy [unifyRel_def,lex_prod_def, inv_image_def]
"!!x. ((X,Y), (Comb A (Comb B C), Comb D (Comb E F))) : unifyRel ==> \
\ ((X,Y), (Comb (Comb A B) C, Comb (Comb D E) F)) : unifyRel";
-by (asm_full_simp_tac (!simpset addsimps [uterm_less_def, measure_def, rprod_def,
+by (asm_full_simp_tac (!simpset addsimps [measure_def,
less_eq, inv_image_def,add_assoc]) 1);
by (subgoal_tac "(vars_of A Un vars_of B Un vars_of C Un \
\ (vars_of D Un vars_of E Un vars_of F)) = \
@@ -110,8 +97,7 @@
by (case_tac "x: (vars_of N1 Un vars_of N2)" 1);
(*uterm_less case*)
by (asm_simp_tac
- (!simpset addsimps [less_eq, unifyRel_def, uterm_less_def,
- rprod_def, lex_prod_def,
+ (!simpset addsimps [less_eq, unifyRel_def, lex_prod_def,
measure_def, inv_image_def]) 1);
by (Blast_tac 1);
(*finite_psubset case*)
@@ -155,9 +141,19 @@
(*---------------------------------------------------------------------------
+ * Eliminate tc0 from the recursion equations and the induction theorem.
+ *---------------------------------------------------------------------------*)
+val [wfr,tc] = Prim.Rules.CONJUNCTS tc0;
+val unifyRules0 = map (normalize_thm [fn th => wfr RS th, fn th => tc RS th])
+ unify.rules;
+
+val unifyInduct0 = [wfr,tc] MRS unify.induct;
+
+
+(*---------------------------------------------------------------------------
* The nested TC. Proved by recursion induction.
*---------------------------------------------------------------------------*)
-val [tc1,tc2,tc3] = unify.tcs;
+val [_,_,tc3] = unify.tcs;
goalw_cterm [] (cterm_of (sign_of Unify.thy) (HOLogic.mk_Trueprop tc3));
(*---------------------------------------------------------------------------
* The extracted TC needs the scope of its quantifiers adjusted, so our
@@ -177,7 +173,7 @@
(*Const-Const case*)
by (simp_tac
(!simpset addsimps [unifyRel_def, lex_prod_def, measure_def,
- inv_image_def, less_eq, uterm_less_def, rprod_def]) 1);
+ inv_image_def, less_eq]) 1);
(** LEVEL 7 **)
(*Comb-Comb case*)
by (subst_case_tac "unify(M1a, M2a)");
@@ -194,7 +190,7 @@
by (asm_simp_tac HOL_ss 2);
by (rtac Rassoc 1);
by (Blast_tac 1);
-qed_spec_mp "unify_TC2";
+qed_spec_mp "unify_TC";
(*---------------------------------------------------------------------------
@@ -211,7 +207,7 @@
\ | Subst sigma => Subst (theta <> sigma)))";
by (asm_simp_tac (!simpset addsimps unifyRules0) 1);
by (subst_case_tac "unify(M1, M2)");
-by (asm_simp_tac (!simpset addsimps [unify_TC2]) 1);
+by (asm_simp_tac (!simpset addsimps [unify_TC]) 1);
qed "unifyCombComb";
@@ -219,20 +215,10 @@
Addsimps unifyRules;
-val prems = goal Unify.thy
-" [| !!m n. Q (Const m) (Const n); \
-\ !!m M N. Q (Const m) (Comb M N); !!m x. Q (Const m) (Var x); \
-\ !!x M. Q (Var x) M; !!M N x. Q (Comb M N) (Const x); \
-\ !!M N x. Q (Comb M N) (Var x); \
-\ !!M1 N1 M2 N2. \
-\ (! theta. \
-\ unify (M1, M2) = Subst theta --> \
-\ Q (N1 <| theta) (N2 <| theta)) & Q M1 M2 \
-\ ==> Q (Comb M1 N1) (Comb M2 N2) |] ==> Q M1 M2";
-by (res_inst_tac [("v","M1"),("v1.0","M2")] unifyInduct0 1);
-by (ALLGOALS (asm_simp_tac (!simpset addsimps (unify_TC2::prems))));
-qed "unifyInduct";
-
+bind_thm ("unifyInduct",
+ rule_by_tactic
+ (ALLGOALS (full_simp_tac (!simpset addsimps [unify_TC])))
+ unifyInduct0);
(*---------------------------------------------------------------------------
@@ -242,8 +228,8 @@
* approach of M&W, who used idempotence and MGU-ness in the termination proof.
*---------------------------------------------------------------------------*)
-goal Unify.thy "!theta. unify(P,Q) = Subst theta --> MGUnifier theta P Q";
-by (res_inst_tac [("M1.0","P"),("M2.0","Q")] unifyInduct 1);
+goal Unify.thy "!theta. unify(M,N) = Subst theta --> MGUnifier theta M N";
+by (res_inst_tac [("v","M"),("v1.0","N")] unifyInduct 1);
by (ALLGOALS (asm_simp_tac (!simpset setloop split_tac [expand_if])));
(*Const-Const case*)
by (simp_tac (!simpset addsimps [MGUnifier_def,Unifier_def]) 1);
@@ -273,8 +259,8 @@
by (eres_inst_tac [("x","delta")] allE 1);
by (subgoal_tac "N1 <| theta <| delta = N2 <| theta <| delta" 1);
(*Proving the subgoal*)
-by (full_simp_tac (!simpset addsimps [subst_eq_iff]) 2);
-by (blast_tac (!claset addIs [trans,sym] delrules [impCE]) 2);
+by (full_simp_tac (!simpset addsimps [subst_eq_iff]) 2
+ THEN blast_tac (!claset addIs [trans,sym] delrules [impCE]) 2);
by (blast_tac (!claset addIs [subst_trans, subst_cong,
comp_assoc RS subst_sym]) 1);
qed_spec_mp "unify_gives_MGU";
@@ -283,30 +269,19 @@
(*---------------------------------------------------------------------------
* Unify returns idempotent substitutions, when it succeeds.
*---------------------------------------------------------------------------*)
-goal Unify.thy "!theta. unify(P,Q) = Subst theta --> Idem theta";
-by (res_inst_tac [("M1.0","P"),("M2.0","Q")] unifyInduct 1);
+goal Unify.thy "!theta. unify(M,N) = Subst theta --> Idem theta";
+by (res_inst_tac [("v","M"),("v1.0","N")] unifyInduct 1);
by (ALLGOALS (asm_simp_tac (!simpset addsimps [Var_Idem]
setloop split_tac[expand_if])));
(*Comb-Comb case*)
by (safe_tac (!claset));
by (subst_case_tac "unify(M1, M2)");
by (subst_case_tac "unify(N1 <| list, N2 <| list)");
-by (hyp_subst_tac 1);
-by prune_params_tac;
-by (rename_tac "theta sigma" 1);
-(** LEVEL 8 **)
-by (dtac unify_gives_MGU 1);
-by (dtac unify_gives_MGU 1);
-by (rewrite_tac [MGUnifier_def]);
-by (safe_tac (!claset));
+by (safe_tac (!claset addSDs [rewrite_rule [MGUnifier_def] unify_gives_MGU]));
by (rtac Idem_comp 1);
by (atac 1);
by (atac 1);
-
-by (eres_inst_tac [("x","q")] allE 1);
-by (asm_full_simp_tac (!simpset addsimps [MoreGeneral_def]) 1);
-by (safe_tac (!claset));
-by (asm_full_simp_tac
- (!simpset addsimps [srange_iff, subst_eq_iff, Idem_def]) 1);
+by (best_tac (!claset addss (!simpset addsimps
+ [MoreGeneral_def, subst_eq_iff, Idem_def])) 1);
qed_spec_mp "unify_gives_Idem";