Now uses type option instead of Fail/Subst
authorpaulson
Thu May 22 15:10:59 1997 +0200 (1997-05-22)
changeset 32998adf24153732
parent 3298 5f0ed3caa991
child 3300 4f5ffefa7799
Now uses type option instead of Fail/Subst
No references to wf_rel_prod
src/HOL/Subst/Unify.ML
     1.1 --- a/src/HOL/Subst/Unify.ML	Thu May 22 15:10:37 1997 +0200
     1.2 +++ b/src/HOL/Subst/Unify.ML	Thu May 22 15:10:59 1997 +0200
     1.3 @@ -42,7 +42,7 @@
     1.4  (* Wellfoundedness of unifyRel *)
     1.5  by (simp_tac (!simpset addsimps [unifyRel_def,
     1.6  				 wf_inv_image, wf_lex_prod, wf_finite_psubset,
     1.7 -				 wf_rel_prod, wf_measure]) 1);
     1.8 +				 wf_measure]) 1);
     1.9  (* TC *)
    1.10  by (Step_tac 1);
    1.11  by (simp_tac (!simpset addsimps [finite_psubset_def, finite_vars_of,
    1.12 @@ -124,22 +124,6 @@
    1.13  qed "var_elimR";
    1.14  
    1.15  
    1.16 -val Some{nchotomy = subst_nchotomy,...} = assoc(!datatypes,"subst");
    1.17 -
    1.18 -(*---------------------------------------------------------------------------
    1.19 - * Do a case analysis on something of type 'a subst. 
    1.20 - *---------------------------------------------------------------------------*)
    1.21 -
    1.22 -fun subst_case_tac t =
    1.23 -(cut_inst_tac [("x",t)] (subst_nchotomy RS spec) 1 
    1.24 -  THEN etac disjE 1 
    1.25 -  THEN rotate_tac ~1 1 
    1.26 -  THEN Asm_full_simp_tac 1 
    1.27 -  THEN etac exE 1
    1.28 -  THEN rotate_tac ~1 1 
    1.29 -  THEN Asm_full_simp_tac 1);
    1.30 -
    1.31 -
    1.32  (*---------------------------------------------------------------------------
    1.33   * Eliminate tc0 from the recursion equations and the induction theorem.
    1.34   *---------------------------------------------------------------------------*)
    1.35 @@ -160,13 +144,13 @@
    1.36   * first step is to restrict the scopes of N1 and N2.
    1.37   *---------------------------------------------------------------------------*)
    1.38  by (subgoal_tac "!M1 M2 theta.  \
    1.39 - \   unify(M1, M2) = Subst theta --> \
    1.40 + \   unify(M1, M2) = Some theta --> \
    1.41   \   (!N1 N2. ((N1<|theta, N2<|theta), Comb M1 N1, Comb M2 N2) : unifyRel)" 1);
    1.42  by (Blast_tac 1);
    1.43  by (rtac allI 1); 
    1.44  by (rtac allI 1);
    1.45  (* Apply induction *)
    1.46 -by (res_inst_tac [("v","M1"),("v1.0","M2")] unifyInduct0 1);
    1.47 +by (res_inst_tac [("u","M1"),("v","M2")] unifyInduct0 1);
    1.48  by (ALLGOALS 
    1.49      (asm_simp_tac (!simpset addsimps (var_elimR::unifyRules0)
    1.50  			    setloop (split_tac [expand_if]))));
    1.51 @@ -176,9 +160,9 @@
    1.52  			inv_image_def, less_eq]) 1);
    1.53  (** LEVEL 7 **)
    1.54  (*Comb-Comb case*)
    1.55 -by (subst_case_tac "unify(M1a, M2a)");
    1.56 +by (option_case_tac "unify(M1a, M2a)" 1);
    1.57  by (rename_tac "theta" 1);
    1.58 -by (subst_case_tac "unify(N1 <| theta, N2 <| theta)");
    1.59 +by (option_case_tac "unify(N1 <| theta, N2 <| theta)" 1);
    1.60  by (rename_tac "sigma" 1);
    1.61  by (REPEAT (rtac allI 1));
    1.62  by (rename_tac "P Q" 1); 
    1.63 @@ -201,12 +185,12 @@
    1.64  goal Unify.thy 
    1.65    "unify(Comb M1 N1, Comb M2 N2) =      \
    1.66  \      (case unify(M1,M2)               \
    1.67 -\        of Fail => Fail                \
    1.68 -\         | Subst theta => (case unify(N1 <| theta, N2 <| theta)        \
    1.69 -\                            of Fail => Fail    \
    1.70 -\                             | Subst sigma => Subst (theta <> sigma)))";
    1.71 +\        of None => None                \
    1.72 +\         | Some theta => (case unify(N1 <| theta, N2 <| theta)        \
    1.73 +\                            of None => None    \
    1.74 +\                             | Some sigma => Some (theta <> sigma)))";
    1.75  by (asm_simp_tac (!simpset addsimps unifyRules0) 1);
    1.76 -by (subst_case_tac "unify(M1, M2)");
    1.77 +by (option_case_tac "unify(M1, M2)" 1);
    1.78  by (asm_simp_tac (!simpset addsimps [unify_TC]) 1);
    1.79  qed "unifyCombComb";
    1.80  
    1.81 @@ -228,8 +212,8 @@
    1.82   * approach of M&W, who used idempotence and MGU-ness in the termination proof.
    1.83   *---------------------------------------------------------------------------*)
    1.84  
    1.85 -goal Unify.thy "!theta. unify(M,N) = Subst theta --> MGUnifier theta M N";
    1.86 -by (res_inst_tac [("v","M"),("v1.0","N")] unifyInduct 1);
    1.87 +goal Unify.thy "!theta. unify(M,N) = Some theta --> MGUnifier theta M N";
    1.88 +by (res_inst_tac [("u","M"),("v","N")] unifyInduct 1);
    1.89  by (ALLGOALS (asm_simp_tac (!simpset setloop split_tac [expand_if])));
    1.90  (*Const-Const case*)
    1.91  by (simp_tac (!simpset addsimps [MGUnifier_def,Unifier_def]) 1);
    1.92 @@ -243,8 +227,8 @@
    1.93  by (simp_tac (!simpset addsimps [MGUnifier_Var]) 1);
    1.94  (*Comb-Comb case*)
    1.95  by (safe_tac (!claset));
    1.96 -by (subst_case_tac "unify(M1, M2)");
    1.97 -by (subst_case_tac "unify(N1<|list, N2<|list)");
    1.98 +by (option_case_tac "unify(M1, M2)" 1);
    1.99 +by (option_case_tac "unify(N1 <| a, N2 <| a)" 1);
   1.100  by (hyp_subst_tac 1);
   1.101  by (asm_full_simp_tac (!simpset addsimps [MGUnifier_def, Unifier_def])1);
   1.102  (** LEVEL 13 **)
   1.103 @@ -269,14 +253,14 @@
   1.104  (*---------------------------------------------------------------------------
   1.105   * Unify returns idempotent substitutions, when it succeeds.
   1.106   *---------------------------------------------------------------------------*)
   1.107 -goal Unify.thy "!theta. unify(M,N) = Subst theta --> Idem theta";
   1.108 -by (res_inst_tac [("v","M"),("v1.0","N")] unifyInduct 1);
   1.109 +goal Unify.thy "!theta. unify(M,N) = Some theta --> Idem theta";
   1.110 +by (res_inst_tac [("u","M"),("v","N")] unifyInduct 1);
   1.111  by (ALLGOALS (asm_simp_tac (!simpset addsimps [Var_Idem] 
   1.112  			             setloop split_tac[expand_if])));
   1.113  (*Comb-Comb case*)
   1.114  by (safe_tac (!claset));
   1.115 -by (subst_case_tac "unify(M1, M2)");
   1.116 -by (subst_case_tac "unify(N1 <| list, N2 <| list)");
   1.117 +by (option_case_tac "unify(M1, M2)" 1);
   1.118 +by (option_case_tac "unify(N1 <| a, N2 <| a)" 1);
   1.119  by (safe_tac (!claset addSDs [rewrite_rule [MGUnifier_def] unify_gives_MGU]));
   1.120  by (rtac Idem_comp 1);
   1.121  by (atac 1);