# HG changeset patch # User paulson # Date 864306659 -7200 # Node ID 8adf24153732d4f09eae0e5223e220bcf70c7cb8 # Parent 5f0ed3caa99158705a6418a6b147f992890277da Now uses type option instead of Fail/Subst No references to wf_rel_prod diff -r 5f0ed3caa991 -r 8adf24153732 src/HOL/Subst/Unify.ML --- a/src/HOL/Subst/Unify.ML Thu May 22 15:10:37 1997 +0200 +++ b/src/HOL/Subst/Unify.ML Thu May 22 15:10:59 1997 +0200 @@ -42,7 +42,7 @@ (* Wellfoundedness of unifyRel *) by (simp_tac (!simpset addsimps [unifyRel_def, wf_inv_image, wf_lex_prod, wf_finite_psubset, - wf_rel_prod, wf_measure]) 1); + wf_measure]) 1); (* TC *) by (Step_tac 1); by (simp_tac (!simpset addsimps [finite_psubset_def, finite_vars_of, @@ -124,22 +124,6 @@ qed "var_elimR"; -val Some{nchotomy = subst_nchotomy,...} = assoc(!datatypes,"subst"); - -(*--------------------------------------------------------------------------- - * Do a case analysis on something of type 'a subst. - *---------------------------------------------------------------------------*) - -fun subst_case_tac t = -(cut_inst_tac [("x",t)] (subst_nchotomy RS spec) 1 - THEN etac disjE 1 - THEN rotate_tac ~1 1 - THEN Asm_full_simp_tac 1 - THEN etac exE 1 - THEN rotate_tac ~1 1 - THEN Asm_full_simp_tac 1); - - (*--------------------------------------------------------------------------- * Eliminate tc0 from the recursion equations and the induction theorem. *---------------------------------------------------------------------------*) @@ -160,13 +144,13 @@ * first step is to restrict the scopes of N1 and N2. *---------------------------------------------------------------------------*) by (subgoal_tac "!M1 M2 theta. \ - \ unify(M1, M2) = Subst theta --> \ + \ unify(M1, M2) = Some theta --> \ \ (!N1 N2. ((N1<|theta, N2<|theta), Comb M1 N1, Comb M2 N2) : unifyRel)" 1); by (Blast_tac 1); by (rtac allI 1); by (rtac allI 1); (* Apply induction *) -by (res_inst_tac [("v","M1"),("v1.0","M2")] unifyInduct0 1); +by (res_inst_tac [("u","M1"),("v","M2")] unifyInduct0 1); by (ALLGOALS (asm_simp_tac (!simpset addsimps (var_elimR::unifyRules0) setloop (split_tac [expand_if])))); @@ -176,9 +160,9 @@ inv_image_def, less_eq]) 1); (** LEVEL 7 **) (*Comb-Comb case*) -by (subst_case_tac "unify(M1a, M2a)"); +by (option_case_tac "unify(M1a, M2a)" 1); by (rename_tac "theta" 1); -by (subst_case_tac "unify(N1 <| theta, N2 <| theta)"); +by (option_case_tac "unify(N1 <| theta, N2 <| theta)" 1); by (rename_tac "sigma" 1); by (REPEAT (rtac allI 1)); by (rename_tac "P Q" 1); @@ -201,12 +185,12 @@ goal Unify.thy "unify(Comb M1 N1, Comb M2 N2) = \ \ (case unify(M1,M2) \ -\ of Fail => Fail \ -\ | Subst theta => (case unify(N1 <| theta, N2 <| theta) \ -\ of Fail => Fail \ -\ | Subst sigma => Subst (theta <> sigma)))"; +\ of None => None \ +\ | Some theta => (case unify(N1 <| theta, N2 <| theta) \ +\ of None => None \ +\ | Some sigma => Some (theta <> sigma)))"; by (asm_simp_tac (!simpset addsimps unifyRules0) 1); -by (subst_case_tac "unify(M1, M2)"); +by (option_case_tac "unify(M1, M2)" 1); by (asm_simp_tac (!simpset addsimps [unify_TC]) 1); qed "unifyCombComb"; @@ -228,8 +212,8 @@ * approach of M&W, who used idempotence and MGU-ness in the termination proof. *---------------------------------------------------------------------------*) -goal Unify.thy "!theta. unify(M,N) = Subst theta --> MGUnifier theta M N"; -by (res_inst_tac [("v","M"),("v1.0","N")] unifyInduct 1); +goal Unify.thy "!theta. unify(M,N) = Some theta --> MGUnifier theta M N"; +by (res_inst_tac [("u","M"),("v","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); @@ -243,8 +227,8 @@ by (simp_tac (!simpset addsimps [MGUnifier_Var]) 1); (*Comb-Comb case*) by (safe_tac (!claset)); -by (subst_case_tac "unify(M1, M2)"); -by (subst_case_tac "unify(N1<|list, N2<|list)"); +by (option_case_tac "unify(M1, M2)" 1); +by (option_case_tac "unify(N1 <| a, N2 <| a)" 1); by (hyp_subst_tac 1); by (asm_full_simp_tac (!simpset addsimps [MGUnifier_def, Unifier_def])1); (** LEVEL 13 **) @@ -269,14 +253,14 @@ (*--------------------------------------------------------------------------- * Unify returns idempotent substitutions, when it succeeds. *---------------------------------------------------------------------------*) -goal Unify.thy "!theta. unify(M,N) = Subst theta --> Idem theta"; -by (res_inst_tac [("v","M"),("v1.0","N")] unifyInduct 1); +goal Unify.thy "!theta. unify(M,N) = Some theta --> Idem theta"; +by (res_inst_tac [("u","M"),("v","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 (option_case_tac "unify(M1, M2)" 1); +by (option_case_tac "unify(N1 <| a, N2 <| a)" 1); by (safe_tac (!claset addSDs [rewrite_rule [MGUnifier_def] unify_gives_MGU])); by (rtac Idem_comp 1); by (atac 1);