# HG changeset patch
# User paulson
# Date 864204782 -7200
# Node ID 89e5f4163663a28b8bfe0aaa958657e99e460aa8
# Parent  8358e19d0d4cdcaf2c7a238d2f52ad398d78e48f
Removed rprod from the WF relation; simplified proofs;
induction rule is now curried

diff -r 8358e19d0d4c -r 89e5f4163663 src/HOL/Subst/Unify.ML
--- 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";