src/FOLP/simp.ML
changeset 32449 696d64ed85da
parent 32091 30e2ffbba718
child 32740 9dd0a2f83429
     1.1 --- a/src/FOLP/simp.ML	Sat Aug 29 10:50:04 2009 +0200
     1.2 +++ b/src/FOLP/simp.ML	Sat Aug 29 12:01:25 2009 +0200
     1.3 @@ -52,7 +52,7 @@
     1.4    val tracing   : bool ref
     1.5  end;
     1.6  
     1.7 -functor SimpFun (Simp_data: SIMP_DATA) : SIMP = 
     1.8 +functor SimpFun (Simp_data: SIMP_DATA) : SIMP =
     1.9  struct
    1.10  
    1.11  local open Simp_data in
    1.12 @@ -74,12 +74,12 @@
    1.13    Similar to match_from_nat_tac, but the net does not contain numbers;
    1.14    rewrite rules are not ordered.*)
    1.15  fun net_tac net =
    1.16 -  SUBGOAL(fn (prem,i) => 
    1.17 +  SUBGOAL(fn (prem,i) =>
    1.18            resolve_tac (Net.unify_term net (Logic.strip_assums_concl prem)) i);
    1.19  
    1.20  (*match subgoal i against possible theorems indexed by lhs in the net*)
    1.21  fun lhs_net_tac net =
    1.22 -  SUBGOAL(fn (prem,i) => 
    1.23 +  SUBGOAL(fn (prem,i) =>
    1.24            biresolve_tac (Net.unify_term net
    1.25                         (lhs_of (Logic.strip_assums_concl prem))) i);
    1.26  
    1.27 @@ -110,7 +110,7 @@
    1.28  
    1.29  (*Get the norm constants from norm_thms*)
    1.30  val norms =
    1.31 -  let fun norm thm = 
    1.32 +  let fun norm thm =
    1.33        case lhs_of(concl_of thm) of
    1.34            Const(n,_)$_ => n
    1.35          | _ => error "No constant in lhs of a norm_thm"
    1.36 @@ -144,7 +144,7 @@
    1.37  (**** Adding "NORM" tags ****)
    1.38  
    1.39  (*get name of the constant from conclusion of a congruence rule*)
    1.40 -fun cong_const cong = 
    1.41 +fun cong_const cong =
    1.42      case head_of (lhs_of (concl_of cong)) of
    1.43          Const(c,_) => c
    1.44        | _ => ""                 (*a placeholder distinct from const names*);
    1.45 @@ -156,9 +156,9 @@
    1.46  fun add_hidden_vars ccs =
    1.47    let fun add_hvars tm hvars = case tm of
    1.48                Abs(_,_,body) => OldTerm.add_term_vars(body,hvars)
    1.49 -            | _$_ => let val (f,args) = strip_comb tm 
    1.50 +            | _$_ => let val (f,args) = strip_comb tm
    1.51                       in case f of
    1.52 -                            Const(c,T) => 
    1.53 +                            Const(c,T) =>
    1.54                                  if member (op =) ccs c
    1.55                                  then fold_rev add_hvars args hvars
    1.56                                  else OldTerm.add_term_vars (tm, hvars)
    1.57 @@ -202,13 +202,13 @@
    1.58      val hvs = map (#1 o dest_Var) hvars
    1.59      val refl1_tac = refl_tac 1
    1.60      fun norm_step_tac st = st |>
    1.61 -	 (case head_of(rhs_of_eq 1 st) of
    1.62 -	    Var(ixn,_) => if ixn mem hvs then refl1_tac
    1.63 -			  else resolve_tac normI_thms 1 ORELSE refl1_tac
    1.64 -	  | Const _ => resolve_tac normI_thms 1 ORELSE
    1.65 -		       resolve_tac congs 1 ORELSE refl1_tac
    1.66 -	  | Free _ => resolve_tac congs 1 ORELSE refl1_tac
    1.67 -	  | _ => refl1_tac)
    1.68 +         (case head_of(rhs_of_eq 1 st) of
    1.69 +            Var(ixn,_) => if ixn mem hvs then refl1_tac
    1.70 +                          else resolve_tac normI_thms 1 ORELSE refl1_tac
    1.71 +          | Const _ => resolve_tac normI_thms 1 ORELSE
    1.72 +                       resolve_tac congs 1 ORELSE refl1_tac
    1.73 +          | Free _ => resolve_tac congs 1 ORELSE refl1_tac
    1.74 +          | _ => refl1_tac)
    1.75      val add_norm_tac = DEPTH_FIRST (has_fewer_prems nops) norm_step_tac
    1.76      val SOME(thm'',_) = Seq.pull(add_norm_tac thm')
    1.77  in thm'' end;
    1.78 @@ -246,9 +246,9 @@
    1.79  (** Insertion of congruences and rewrites **)
    1.80  
    1.81  (*insert a thm in a thm net*)
    1.82 -fun insert_thm_warn th net = 
    1.83 +fun insert_thm_warn th net =
    1.84    Net.insert_term Thm.eq_thm_prop (concl_of th, th) net
    1.85 -  handle Net.INSERT => 
    1.86 +  handle Net.INSERT =>
    1.87      (writeln ("Duplicate rewrite or congruence rule:\n" ^
    1.88          Display.string_of_thm_without_context th); net);
    1.89  
    1.90 @@ -272,9 +272,9 @@
    1.91  (** Deletion of congruences and rewrites **)
    1.92  
    1.93  (*delete a thm from a thm net*)
    1.94 -fun delete_thm_warn th net = 
    1.95 +fun delete_thm_warn th net =
    1.96    Net.delete_term Thm.eq_thm_prop (concl_of th, th) net
    1.97 -  handle Net.DELETE => 
    1.98 +  handle Net.DELETE =>
    1.99      (writeln ("No such rewrite or congruence rule:\n" ^
   1.100          Display.string_of_thm_without_context th); net);
   1.101  
   1.102 @@ -337,17 +337,17 @@
   1.103      in find_if(tm,0) end;
   1.104  
   1.105  fun IF1_TAC cong_tac i =
   1.106 -    let fun seq_try (ifth::ifths,ifc::ifcs) thm = 
   1.107 +    let fun seq_try (ifth::ifths,ifc::ifcs) thm =
   1.108                  (COND (if_rewritable ifc i) (DETERM(rtac ifth i))
   1.109                          (seq_try(ifths,ifcs))) thm
   1.110                | seq_try([],_) thm = no_tac thm
   1.111          and try_rew thm = (seq_try(case_rews,case_consts) ORELSE one_subt) thm
   1.112          and one_subt thm =
   1.113                  let val test = has_fewer_prems (nprems_of thm + 1)
   1.114 -                    fun loop thm = 
   1.115 -			COND test no_tac
   1.116 +                    fun loop thm =
   1.117 +                        COND test no_tac
   1.118                            ((try_rew THEN DEPTH_FIRST test (refl_tac i))
   1.119 -			   ORELSE (refl_tac i THEN loop)) thm
   1.120 +                           ORELSE (refl_tac i THEN loop)) thm
   1.121                  in (cong_tac THEN loop) thm end
   1.122      in COND (may_match(case_consts,i)) try_rew no_tac end;
   1.123  
   1.124 @@ -381,12 +381,12 @@
   1.125  
   1.126  (*print lhs of conclusion of subgoal i*)
   1.127  fun pr_goal_lhs i st =
   1.128 -    writeln (Syntax.string_of_term_global (Thm.theory_of_thm st) 
   1.129 +    writeln (Syntax.string_of_term_global (Thm.theory_of_thm st)
   1.130               (lhs_of (prepare_goal i st)));
   1.131  
   1.132  (*print conclusion of subgoal i*)
   1.133  fun pr_goal_concl i st =
   1.134 -    writeln (Syntax.string_of_term_global (Thm.theory_of_thm st) (prepare_goal i st)) 
   1.135 +    writeln (Syntax.string_of_term_global (Thm.theory_of_thm st) (prepare_goal i st))
   1.136  
   1.137  (*print subgoals i to j (inclusive)*)
   1.138  fun pr_goals (i,j) st =
   1.139 @@ -439,7 +439,7 @@
   1.140          then writeln (cat_lines
   1.141            ("Adding rewrites:" :: map Display.string_of_thm_without_context new_rws))
   1.142          else ();
   1.143 -        (ss,thm,anet',anet::ats,cs) 
   1.144 +        (ss,thm,anet',anet::ats,cs)
   1.145      end;
   1.146  
   1.147  fun rew(seq,thm,ss,anet,ats,cs, more) = case Seq.pull seq of
   1.148 @@ -492,7 +492,7 @@
   1.149  
   1.150  fun EXEC_TAC(ss,fl) (SS{auto_tac,cong_net,simp_net,...}) =
   1.151  let val cong_tac = net_tac cong_net
   1.152 -in fn i => 
   1.153 +in fn i =>
   1.154      (fn thm =>
   1.155       if i <= 0 orelse nprems_of thm < i then Seq.empty
   1.156       else Seq.single(execute(ss,fl,auto_tac,cong_tac,simp_net,i,thm)))