TFL/post.sml
changeset 6498 1ebbe18fe236
parent 6476 92d142e58a5b
child 6524 13410ecfce0b
--- a/TFL/post.sml	Fri Apr 23 12:22:30 1999 +0200
+++ b/TFL/post.sml	Fri Apr 23 12:23:21 1999 +0200
@@ -23,15 +23,18 @@
    val define   : theory -> xstring -> string -> string list 
                   -> theory * Prim.pattern list
 
+   val function_i : theory -> xstring 
+                  -> thm list (* congruence rules *)
+                  -> term list -> theory * thm
+
+   val function : theory -> xstring 
+                  -> thm list 
+                  -> string list -> theory * thm
+
    val simplify_defn : simpset * thm list 
                         -> theory * (string * Prim.pattern list)
                         -> {rules:thm list, induct:thm, tcs:term list}
 
-  (*-------------------------------------------------------------------------
-       val function : theory -> term -> {theory:theory, eq_ind : thm}
-       val lazyR_def: theory -> term -> {theory:theory, eqns : thm}
-   *-------------------------------------------------------------------------*)
-
   end;
 
 
@@ -40,216 +43,217 @@
  structure Prim = Prim
  structure S = USyntax
 
-(*---------------------------------------------------------------------------
- * Extract termination goals so that they can be put it into a goalstack, or 
- * have a tactic directly applied to them.
- *--------------------------------------------------------------------------*)
-fun termination_goals rules = 
-    map (#1 o Type.freeze_thaw o HOLogic.dest_Trueprop)
-      (foldr (fn (th,A) => union_term (prems_of th, A)) (rules, []));
+ val trace = Prim.trace
+
+ (*---------------------------------------------------------------------------
+  * Extract termination goals so that they can be put it into a goalstack, or 
+  * have a tactic directly applied to them.
+  *--------------------------------------------------------------------------*)
+ fun termination_goals rules = 
+     map (#1 o Type.freeze_thaw o HOLogic.dest_Trueprop)
+       (foldr (fn (th,A) => union_term (prems_of th, A)) (rules, []));
 
-(*---------------------------------------------------------------------------
- * Finds the termination conditions in (highly massaged) definition and 
- * puts them into a goalstack.
+ (*---------------------------------------------------------------------------
+  * Finds the termination conditions in (highly massaged) definition and 
+  * puts them into a goalstack.
+  *--------------------------------------------------------------------------*)
+ fun tgoalw thy defs rules = 
+   case termination_goals rules of
+       [] => error "tgoalw: no termination conditions to prove"
+     | L  => goalw_cterm defs 
+	       (Thm.cterm_of (Theory.sign_of thy) 
+			 (HOLogic.mk_Trueprop(USyntax.list_mk_conj L)));
+
+ fun tgoal thy = tgoalw thy [];
+
+ (*---------------------------------------------------------------------------
+ * Three postprocessors are applied to the definition.  It
+ * attempts to prove wellfoundedness of the given relation, simplifies the
+ * non-proved termination conditions, and finally attempts to prove the 
+ * simplified termination conditions.
  *--------------------------------------------------------------------------*)
-fun tgoalw thy defs rules = 
-  case termination_goals rules of
-      [] => error "tgoalw: no termination conditions to prove"
-    | L  => goalw_cterm defs 
-              (Thm.cterm_of (Theory.sign_of thy) 
-	                (HOLogic.mk_Trueprop(USyntax.list_mk_conj L)));
-
-fun tgoal thy = tgoalw thy [];
-
-(*---------------------------------------------------------------------------
-* Three postprocessors are applied to the definition.  It
-* attempts to prove wellfoundedness of the given relation, simplifies the
-* non-proved termination conditions, and finally attempts to prove the 
-* simplified termination conditions.
-*--------------------------------------------------------------------------*)
-fun std_postprocessor ss =
-  Prim.postprocess
-   {WFtac      = REPEAT (ares_tac [wf_empty, wf_measure, wf_inv_image, 
-				   wf_lex_prod, wf_less_than, wf_trancl] 1),
-    terminator = asm_simp_tac ss 1
-		 THEN TRY(CLASET' (fn cs => best_tac
-			  (cs addSDs [not0_implies_Suc] addss ss)) 1),
-    simplifier = Rules.simpl_conv ss []};
+ fun std_postprocessor ss =
+   Prim.postprocess
+    {WFtac      = REPEAT (ares_tac [wf_empty, wf_pred_nat, 
+				    wf_measure, wf_inv_image, 
+				    wf_lex_prod, wf_less_than, wf_trancl] 1),
+     terminator = asm_simp_tac ss 1
+		  THEN TRY(CLASET' (fn cs => best_tac
+			   (cs addSDs [not0_implies_Suc] addss ss)) 1),
+     simplifier = Rules.simpl_conv ss []};
 
 
 
-val concl = #2 o Rules.dest_thm;
+ val concl = #2 o Rules.dest_thm;
 
-(*---------------------------------------------------------------------------
- * Defining a function with an associated termination relation. 
- *---------------------------------------------------------------------------*)
-fun define_i thy fid R eqs = 
-  let val {functional,pats} = Prim.mk_functional thy eqs
-  in (Prim.wfrec_definition0 thy (Sign.base_name fid) R functional, pats)
-  end;
+ (*---------------------------------------------------------------------------
+  * Defining a function with an associated termination relation. 
+  *---------------------------------------------------------------------------*)
+ fun define_i thy fid R eqs = 
+   let val {functional,pats} = Prim.mk_functional thy eqs
+   in (Prim.wfrec_definition0 thy (Sign.base_name fid) R functional, pats)
+   end;
 
-(*lcp's version: takes strings; doesn't return "thm" 
-        (whose signature is a draft and therefore useless) *)
-fun define thy fid R eqs = 
-  let fun read thy = readtm (Theory.sign_of thy) (TVar(("DUMMY",0),[])) 
-  in  define_i thy fid (read thy R) (map (read thy) eqs)  end
-  handle Utils.ERR {mesg,...} => error mesg;
+ fun define thy fid R eqs = 
+   let fun read thy = readtm (Theory.sign_of thy) (TVar(("DUMMY",0),[])) 
+   in  define_i thy fid (read thy R) (map (read thy) eqs)  end
+   handle Utils.ERR {mesg,...} => error mesg;
 
 (*---------------------------------------------------------------------------
  * Postprocess a definition made by "define". This is a separate stage of 
  * processing from the definition stage.
  *---------------------------------------------------------------------------*)
-local 
-structure R = Rules
-structure U = Utils
+ local 
+ structure R = Rules
+ structure U = Utils
 
-(* The rest of these local definitions are for the tricky nested case *)
-val solved = not o U.can S.dest_eq o #2 o S.strip_forall o concl
+ (* The rest of these local definitions are for the tricky nested case *)
+ val solved = not o U.can S.dest_eq o #2 o S.strip_forall o concl
 
-fun id_thm th = 
-   let val {lhs,rhs} = S.dest_eq(#2(S.strip_forall(#2 (R.dest_thm th))))
-   in lhs aconv rhs
-   end handle _ => false
+ fun id_thm th = 
+    let val {lhs,rhs} = S.dest_eq(#2(S.strip_forall(#2 (R.dest_thm th))))
+    in lhs aconv rhs
+    end handle _ => false
 
-fun prover s = prove_goal HOL.thy s (fn _ => [fast_tac HOL_cs 1]);
-val P_imp_P_iff_True = prover "P --> (P= True)" RS mp;
-val P_imp_P_eq_True = P_imp_P_iff_True RS eq_reflection;
-fun mk_meta_eq r = case concl_of r of
-     Const("==",_)$_$_ => r
-  |   _$(Const("op =",_)$_$_) => r RS eq_reflection
-  |   _ => r RS P_imp_P_eq_True
+ fun prover s = prove_goal HOL.thy s (fn _ => [fast_tac HOL_cs 1]);
+ val P_imp_P_iff_True = prover "P --> (P= True)" RS mp;
+ val P_imp_P_eq_True = P_imp_P_iff_True RS eq_reflection;
+ fun mk_meta_eq r = case concl_of r of
+      Const("==",_)$_$_ => r
+   |   _ $(Const("op =",_)$_$_) => r RS eq_reflection
+   |   _ => r RS P_imp_P_eq_True
 
-(*Is this the best way to invoke the simplifier??*)
-fun rewrite L = rewrite_rule (map mk_meta_eq (filter(not o id_thm) L))
+ (*Is this the best way to invoke the simplifier??*)
+ fun rewrite L = rewrite_rule (map mk_meta_eq (filter(not o id_thm) L))
 
-fun join_assums th = 
-  let val {sign,...} = rep_thm th
-      val tych = cterm_of sign
-      val {lhs,rhs} = S.dest_eq(#2 (S.strip_forall (concl th)))
-      val cntxtl = (#1 o S.strip_imp) lhs  (* cntxtl should = cntxtr *)
-      val cntxtr = (#1 o S.strip_imp) rhs  (* but union is solider *)
-      val cntxt = gen_union (op aconv) (cntxtl, cntxtr)
-  in 
-    R.GEN_ALL 
-      (R.DISCH_ALL 
-         (rewrite (map (R.ASSUME o tych) cntxt) (R.SPEC_ALL th)))
-  end
-  val gen_all = S.gen_all
-in
-fun proof_stage ss theory {f, R, rules, full_pats_TCs, TCs} =
-  let val dummy = writeln "Proving induction theorem..  "
-      val ind = Prim.mk_induction theory f R full_pats_TCs
-      val dummy = writeln "Proved induction theorem.\nPostprocessing..  "
-      val {rules, induction, nested_tcs} = 
-	  std_postprocessor ss theory {rules=rules, induction=ind, TCs=TCs}
-  in
-  case nested_tcs
-  of [] => (writeln "Postprocessing done.";
-            {induction=induction, rules=rules,tcs=[]})
-  | L  => let val dummy = writeln "Simplifying nested TCs..  "
-              val (solved,simplified,stubborn) =
-               U.itlist (fn th => fn (So,Si,St) =>
-                     if (id_thm th) then (So, Si, th::St) else
-                     if (solved th) then (th::So, Si, St) 
-                     else (So, th::Si, St)) nested_tcs ([],[],[])
-              val simplified' = map join_assums simplified
-              val rewr = full_simplify (ss addsimps (solved @ simplified'));
-              val induction' = rewr induction
-              and rules'     = rewr rules
-              val dummy = writeln "Postprocessing done."
-          in
-          {induction = induction',
-               rules = rules',
-                 tcs = map (gen_all o S.rhs o #2 o S.strip_forall o concl)
-                           (simplified@stubborn)}
-          end
-  end;
+ fun join_assums th = 
+   let val {sign,...} = rep_thm th
+       val tych = cterm_of sign
+       val {lhs,rhs} = S.dest_eq(#2 (S.strip_forall (concl th)))
+       val cntxtl = (#1 o S.strip_imp) lhs  (* cntxtl should = cntxtr *)
+       val cntxtr = (#1 o S.strip_imp) rhs  (* but union is solider *)
+       val cntxt = gen_union (op aconv) (cntxtl, cntxtr)
+   in 
+     R.GEN_ALL 
+       (R.DISCH_ALL 
+	  (rewrite (map (R.ASSUME o tych) cntxt) (R.SPEC_ALL th)))
+   end
+   val gen_all = S.gen_all
+ in
+ fun proof_stage ss theory {f, R, rules, full_pats_TCs, TCs} =
+   let val dummy = writeln "Proving induction theorem..  "
+       val ind = Prim.mk_induction theory 
+                    {fconst=f, R=R, SV=[], pat_TCs_list=full_pats_TCs}
+       val dummy = writeln "Proved induction theorem.\nPostprocessing..  "
+       val {rules, induction, nested_tcs} = 
+	   std_postprocessor ss theory {rules=rules, induction=ind, TCs=TCs}
+   in
+   case nested_tcs
+   of [] => (writeln "Postprocessing done.";
+	     {induction=induction, rules=rules,tcs=[]})
+   | L  => let val dummy = writeln "Simplifying nested TCs..  "
+	       val (solved,simplified,stubborn) =
+		U.itlist (fn th => fn (So,Si,St) =>
+		      if (id_thm th) then (So, Si, th::St) else
+		      if (solved th) then (th::So, Si, St) 
+		      else (So, th::Si, St)) nested_tcs ([],[],[])
+	       val simplified' = map join_assums simplified
+	       val rewr = full_simplify (ss addsimps (solved @ simplified'));
+	       val induction' = rewr induction
+	       and rules'     = rewr rules
+	       val dummy = writeln "Postprocessing done."
+	   in
+	   {induction = induction',
+		rules = rules',
+		  tcs = map (gen_all o S.rhs o #2 o S.strip_forall o concl)
+			    (simplified@stubborn)}
+	   end
+   end;
 
 
-(*lcp: curry the predicate of the induction rule*)
-fun curry_rule rl = split_rule_var
-                        (head_of (HOLogic.dest_Trueprop (concl_of rl)), 
-			 rl);
-
-(*lcp: put a theorem into Isabelle form, using meta-level connectives*)
-val meta_outer = 
-    curry_rule o standard o 
-    rule_by_tactic (REPEAT 
-		    (FIRSTGOAL (resolve_tac [allI, impI, conjI]
-				ORELSE' etac conjE)));
+ (*lcp: curry the predicate of the induction rule*)
+ fun curry_rule rl = split_rule_var
+			 (head_of (HOLogic.dest_Trueprop (concl_of rl)), 
+			  rl);
 
-(*Strip off the outer !P*)
-val spec'= read_instantiate [("x","P::?'b=>bool")] spec;
-
-val wf_rel_defs = [lex_prod_def, measure_def, inv_image_def];
+ (*lcp: put a theorem into Isabelle form, using meta-level connectives*)
+ val meta_outer = 
+     curry_rule o standard o 
+     rule_by_tactic (REPEAT 
+		     (FIRSTGOAL (resolve_tac [allI, impI, conjI]
+				 ORELSE' etac conjE)));
 
-(*Convert conclusion from = to ==*)
-val eq_reflect_list = map (fn th => (th RS eq_reflection) handle _ => th);
+ (*Strip off the outer !P*)
+ val spec'= read_instantiate [("x","P::?'b=>bool")] spec;
 
-(*---------------------------------------------------------------------------
- * Install the basic context notions. Others (for nat and list and prod) 
- * have already been added in thry.sml
- *---------------------------------------------------------------------------*)
-val defaultTflCongs = eq_reflect_list [Thms.LET_CONG, if_cong];
+ val wf_rel_defs = [lex_prod_def, measure_def, inv_image_def];
+
+ (*Convert conclusion from = to ==*)
+ val eq_reflect_list = map (fn th => (th RS eq_reflection) handle _ => th);
 
-fun simplify_defn (ss, tflCongs) (thy,(id,pats)) =
-   let val dummy = deny (id mem (Sign.stamp_names_of (Theory.sign_of thy)))
-                        ("Recursive definition " ^ id ^ 
-                         " would clash with the theory of the same name!")
-       val def =  freezeT(get_def thy id)   RS   meta_eq_to_obj_eq
-       val ss' = ss addsimps ((less_Suc_eq RS iffD2) :: wf_rel_defs)
-       val {theory,rules,TCs,full_pats_TCs,patterns} = 
-                Prim.post_definition
-		   (ss', defaultTflCongs @ eq_reflect_list tflCongs)
-		   (thy, (def,pats))
-       val {lhs=f,rhs} = S.dest_eq(concl def)
-       val (_,[R,_]) = S.strip_comb rhs
-       val {induction, rules, tcs} = 
-             proof_stage ss' theory 
-               {f = f, R = R, rules = rules,
-                full_pats_TCs = full_pats_TCs,
-                TCs = TCs}
-       val rules' = map (standard o normalize_thm [RSmp]) (R.CONJUNCTS rules)
-   in  {induct = meta_outer
-                  (normalize_thm [RSspec,RSmp] (induction RS spec')), 
-        rules = rules', 
-        tcs = (termination_goals rules') @ tcs}
-   end
-  handle Utils.ERR {mesg,func,module} => 
-               error (mesg ^ 
-		      "\n    (In TFL function " ^ module ^ "." ^ func ^ ")");
-end;
+ (*---------------------------------------------------------------------------
+  * Install the basic context notions. Others (for nat and list and prod) 
+  * have already been added in thry.sml
+  *---------------------------------------------------------------------------*)
+ fun simplify_defn (ss, tflCongs) (thy,(id,pats)) =
+    let val dummy = deny (id mem (Sign.stamp_names_of (Theory.sign_of thy)))
+			 ("Recursive definition " ^ id ^ 
+			  " would clash with the theory of the same name!")
+	val def = freezeT(get_def thy id)   RS   meta_eq_to_obj_eq
+	val {theory,rules,TCs,full_pats_TCs,patterns} = 
+		 Prim.post_definition (Prim.congs tflCongs)
+		    (thy, (def,pats))
+	val {lhs=f,rhs} = S.dest_eq(concl def)
+	val (_,[R,_]) = S.strip_comb rhs
+	val ss' = ss addsimps Prim.default_simps
+	val {induction, rules, tcs} = 
+	      proof_stage ss' theory 
+		{f = f, R = R, rules = rules,
+		 full_pats_TCs = full_pats_TCs,
+		 TCs = TCs}
+	val rules' = map (standard o normalize_thm [RSmp]) (R.CONJUNCTS rules)
+    in  {induct = meta_outer
+		   (normalize_thm [RSspec,RSmp] (induction RS spec')), 
+	 rules = rules', 
+	 tcs = (termination_goals rules') @ tcs}
+    end
+   handle Utils.ERR {mesg,func,module} => 
+		error (mesg ^ 
+		       "\n    (In TFL function " ^ module ^ "." ^ func ^ ")");
 
 (*---------------------------------------------------------------------------
  *
- *     Definitions with synthesized termination relation temporarily
- *     deleted -- it's not clear how to integrate this facility with
- *     the Isabelle theory file scheme, which restricts
- *     inference at theory-construction time.
- *
-
-local structure R = Rules
-in
-fun function theory eqs = 
- let val dummy = writeln "Making definition..   "
-     val {rules,R,theory,full_pats_TCs,...} = Prim.lazyR_def theory eqs
-     val f = func_of_cond_eqn (concl(R.CONJUNCT1 rules handle _ => rules))
-     val dummy = writeln "Definition made."
-     val dummy = writeln "Proving induction theorem..  "
-     val induction = Prim.mk_induction theory f R full_pats_TCs
-     val dummy = writeln "Induction theorem proved."
- in {theory = theory, 
-     eq_ind = standard (induction RS (rules RS conjI))}
- end
-end;
-
-
-fun lazyR_def theory eqs = 
-   let val {rules,theory, ...} = Prim.lazyR_def theory eqs
-   in {eqns=rules, theory=theory}
-   end
-   handle    e              => print_exn e;
- *
+ *     Definitions with synthesized termination relation
  *
  *---------------------------------------------------------------------------*)
+
+ local open USyntax
+ in 
+ fun func_of_cond_eqn tm =
+   #1(strip_comb(#lhs(dest_eq(#2 (strip_forall(#2(strip_imp tm)))))))
+ end;
+
+ fun function_i thy fid congs eqs = 
+  let val dum = Theory.requires thy "WF_Rel" "recursive function definitions"
+      val {rules,R,theory,full_pats_TCs,SV,...} = 
+	      Prim.lazyR_def thy fid congs eqs
+      val f = func_of_cond_eqn (concl(R.CONJUNCT1 rules handle _ => rules))
+      val dummy = writeln "Definition made.\nProving induction theorem..  "
+      val induction = Prim.mk_induction theory 
+                         {fconst=f, R=R, SV=SV, pat_TCs_list=full_pats_TCs}
+      val dummy = writeln "Induction theorem proved."
+  in (theory, 
+      (*return the conjoined induction rule and recursion equations, 
+	with assumptions remaining to discharge*)
+      standard (induction RS (rules RS conjI)))
+  end
+
+ fun function thy fid congs seqs = 
+   let val _ =  writeln ("Deferred recursive function " ^ fid)
+       fun read thy = readtm (Theory.sign_of thy) (TVar(("DUMMY",0),[])) 
+   in  function_i thy fid congs (map (read thy) seqs)  end
+   handle Utils.ERR {mesg,...} => error mesg;
+
+ end;
+
 end;