processing of tuples in introduction rules
authorbulwahn
Sat Oct 24 16:55:42 2009 +0200 (2009-10-24)
changeset 331130f6e30b87cf1
parent 33112 6672184a736b
child 33114 4785ef554dcc
processing of tuples in introduction rules
src/HOL/ROOT.ML
src/HOL/Tools/Predicate_Compile/pred_compile_aux.ML
src/HOL/Tools/Predicate_Compile/predicate_compile.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
src/HOL/ex/Predicate_Compile.thy
src/HOL/ex/Predicate_Compile_ex.thy
     1.1 --- a/src/HOL/ROOT.ML	Sat Oct 24 16:55:42 2009 +0200
     1.2 +++ b/src/HOL/ROOT.ML	Sat Oct 24 16:55:42 2009 +0200
     1.3 @@ -1,5 +1,6 @@
     1.4  (* Classical Higher-order Logic -- batteries included *)
     1.5  
     1.6 +Toplevel.debug := true;
     1.7  use_thy "Complex_Main";
     1.8  
     1.9  val HOL_proofs = ! Proofterm.proofs;
     2.1 --- a/src/HOL/Tools/Predicate_Compile/pred_compile_aux.ML	Sat Oct 24 16:55:42 2009 +0200
     2.2 +++ b/src/HOL/Tools/Predicate_Compile/pred_compile_aux.ML	Sat Oct 24 16:55:42 2009 +0200
     2.3 @@ -73,8 +73,15 @@
     2.4  
     2.5  (*
     2.6  fun map_atoms f intro = 
     2.7 -fun fold_atoms f intro =
     2.8  *)
     2.9 +fun fold_atoms f intro s =
    2.10 +  let
    2.11 +    val (literals, head) = Logic.strip_horn intro
    2.12 +    fun appl t s = (case t of
    2.13 +      (@{term "Not"} $ t') => f t' s
    2.14 +      | _ => f t s)
    2.15 +  in fold appl (map HOLogic.dest_Trueprop literals) s end
    2.16 +
    2.17  fun fold_map_atoms f intro s =
    2.18    let
    2.19      val (literals, head) = Logic.strip_horn intro
     3.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Sat Oct 24 16:55:42 2009 +0200
     3.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Sat Oct 24 16:55:42 2009 +0200
     3.3 @@ -17,7 +17,73 @@
     3.4  
     3.5  val priority = tracing;
     3.6  
     3.7 +(* tuple processing *)
     3.8 +
     3.9 +fun expand_tuples thy intro =
    3.10 +  let
    3.11 +    fun rewrite_args [] (pats, intro_t, ctxt) = (pats, intro_t, ctxt)
    3.12 +      | rewrite_args (arg::args) (pats, intro_t, ctxt) = 
    3.13 +      (case HOLogic.strip_tupleT (fastype_of arg) of
    3.14 +        (Ts as _ :: _ :: _) =>
    3.15 +        let
    3.16 +          fun rewrite_arg' (Const ("Pair", _) $ _ $ t2, Type ("*", [_, T2]))
    3.17 +            (args, (pats, intro_t, ctxt)) = rewrite_arg' (t2, T2) (args, (pats, intro_t, ctxt))
    3.18 +            | rewrite_arg' (t, Type ("*", [T1, T2])) (args, (pats, intro_t, ctxt)) =
    3.19 +              let
    3.20 +                val ([x, y], ctxt') = Variable.variant_fixes ["x", "y"] ctxt
    3.21 +                val pat = (t, HOLogic.mk_prod (Free (x, T1), Free (y, T2)))
    3.22 +                  (*val _ = tracing ("Rewriting term " ^
    3.23 +                    (Syntax.string_of_term_global thy (fst pat)) ^ " to " ^
    3.24 +                    (Syntax.string_of_term_global thy (snd pat)) ^ " in " ^
    3.25 +                  (Syntax.string_of_term_global thy intro_t))*)
    3.26 +                val intro_t' = Pattern.rewrite_term thy [pat] [] intro_t
    3.27 +                val args' = map (Pattern.rewrite_term thy [pat] []) args
    3.28 +              in
    3.29 +                rewrite_arg' (Free (y, T2), T2) (args', (pat::pats, intro_t', ctxt'))
    3.30 +              end
    3.31 +            | rewrite_arg' _ (args, (pats, intro_t, ctxt)) = (args, (pats, intro_t, ctxt))
    3.32 +          val (args', (pats, intro_t', ctxt')) = rewrite_arg' (arg, fastype_of arg)
    3.33 +            (args, (pats, intro_t, ctxt))
    3.34 +        in
    3.35 +          rewrite_args args' (pats, intro_t', ctxt')
    3.36 +        end
    3.37 +      | _ => rewrite_args args (pats, intro_t, ctxt))
    3.38 +    fun rewrite_prem atom =
    3.39 +      let
    3.40 +        val (_, args) = strip_comb atom
    3.41 +      in rewrite_args args end
    3.42 +    val ctxt = ProofContext.init thy
    3.43 +    val (((T_insts, t_insts), [intro']), ctxt1) = Variable.import false [intro] ctxt
    3.44 +    val intro_t = prop_of intro'
    3.45 +    val concl = Logic.strip_imp_concl intro_t
    3.46 +    val (p, args) = strip_comb (HOLogic.dest_Trueprop concl)
    3.47 +    val (pats', intro_t', ctxt2) = rewrite_args args ([], intro_t, ctxt1)
    3.48 +    val (pats', intro_t', ctxt3) = 
    3.49 +      fold_atoms rewrite_prem intro_t' (pats', intro_t', ctxt2)
    3.50 +    (*val _ = Output.tracing ("intro_t': " ^ (Syntax.string_of_term_global thy intro_t'))
    3.51 +    val _ = Output.tracing ("pats : " ^ (commas (map
    3.52 +      (fn (t1, t2) => (Syntax.string_of_term_global thy t1) ^ " -> " ^
    3.53 +      Syntax.string_of_term_global thy t2) pats'))*)
    3.54 +    fun rewrite_pat (ct1, ct2) =
    3.55 +      (ct1, cterm_of thy (Pattern.rewrite_term thy pats' [] (term_of ct2)))
    3.56 +    val t_insts' = map rewrite_pat t_insts
    3.57 +      (*val _ = Output.tracing ("t_insts':" ^ (commas (map
    3.58 +      (fn (ct1, ct2) => (Syntax.string_of_term_global thy (term_of ct1) ^ " -> " ^
    3.59 +    Syntax.string_of_term_global thy (term_of ct2))) t_insts')))*)
    3.60 +    val intro'' = Thm.instantiate (T_insts, t_insts') intro
    3.61 +      (*val _ = Output.tracing ("intro'':" ^ (Display.string_of_thm_global thy intro''))*)
    3.62 +    val [intro'''] = Variable.export ctxt3 ctxt [intro'']
    3.63 +    (*val _ = Output.tracing ("intro''':" ^ (Display.string_of_thm_global thy intro'''))*)
    3.64 +  in
    3.65 +    intro'''
    3.66 +  end 
    3.67 +
    3.68 +  (* eliminating fst/snd functions *)
    3.69 +val simplify_fst_snd = Simplifier.full_simplify
    3.70 +  (HOL_basic_ss addsimps [@{thm fst_conv}, @{thm snd_conv}, @{thm Pair_eq}])
    3.71 +
    3.72  (* Some last processing *)
    3.73 +
    3.74  fun remove_pointless_clauses intro =
    3.75    if Logic.strip_imp_prems (prop_of intro) = [@{prop "False"}] then
    3.76      []
    3.77 @@ -35,24 +101,25 @@
    3.78        thy |> not (null funnames) ? Predicate_Compile_Fun.define_predicates
    3.79        (get_specs funnames)
    3.80      val _ = priority "Compiling predicates to flat introrules..."
    3.81 -    val (intross, thy'') = apfst flat (fold_map Predicate_Compile_Pred.preprocess
    3.82 +    val (intross1, thy'') = apfst flat (fold_map Predicate_Compile_Pred.preprocess
    3.83        (get_specs prednames) thy')
    3.84      val _ = tracing ("Flattened introduction rules: " ^
    3.85 -      commas (map (Display.string_of_thm_global thy'') (flat intross)))
    3.86 +      commas (map (Display.string_of_thm_global thy'') (flat intross1)))
    3.87      val _ = priority "Replacing functions in introrules..."
    3.88        (*  val _ = burrow (maps (Predicate_Compile_Fun.rewrite_intro thy'')) intross  *)
    3.89 -    val intross' =
    3.90 +    val intross2 =
    3.91        if fail_safe_mode then
    3.92 -        case try (burrow (maps (Predicate_Compile_Fun.rewrite_intro thy''))) intross of
    3.93 -          SOME intross' => intross'
    3.94 -        | NONE => let val _ = warning "Function replacement failed!" in intross end
    3.95 -      else burrow (maps (Predicate_Compile_Fun.rewrite_intro thy'')) intross
    3.96 +        case try (burrow (maps (Predicate_Compile_Fun.rewrite_intro thy''))) intross1 of
    3.97 +          SOME intross => intross
    3.98 +        | NONE => let val _ = warning "Function replacement failed!" in intross1 end
    3.99 +      else burrow (maps (Predicate_Compile_Fun.rewrite_intro thy'')) intross1
   3.100      val _ = tracing ("Introduction rules with replaced functions: " ^
   3.101 -      commas (map (Display.string_of_thm_global thy'') (flat intross')))
   3.102 -    val intross'' = burrow (maps remove_pointless_clauses) intross'
   3.103 -    val intross'' = burrow (map (AxClass.overload thy'')) intross''
   3.104 +      commas (map (Display.string_of_thm_global thy'') (flat intross2)))
   3.105 +    val intross3 = burrow (maps remove_pointless_clauses) intross2
   3.106 +    val intross4 = burrow (map (AxClass.overload thy'')) intross3
   3.107 +    val intross5 = burrow (map (simplify_fst_snd o expand_tuples thy'')) intross4
   3.108      val _ = priority "Registering intro rules..."
   3.109 -    val thy''' = fold Predicate_Compile_Core.register_intros intross'' thy''
   3.110 +    val thy''' = fold Predicate_Compile_Core.register_intros intross5 thy''
   3.111    in
   3.112      thy'''
   3.113    end;
     4.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Sat Oct 24 16:55:42 2009 +0200
     4.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Sat Oct 24 16:55:42 2009 +0200
     4.3 @@ -108,6 +108,7 @@
     4.4    val is_predT : typ -> bool
     4.5    val guess_nparams : typ -> int
     4.6    val cprods_subset : 'a list list -> 'a list list
     4.7 +  val dest_prem : theory -> term list ->  term -> indprem
     4.8  end;
     4.9  
    4.10  structure Predicate_Compile_Core : PREDICATE_COMPILE_CORE =
    4.11 @@ -527,7 +528,7 @@
    4.12      val bigeq = (Thm.symmetric (Conv.implies_concl_conv
    4.13        (MetaSimplifier.rewrite true [@{thm Predicate.eq_is_eq}])
    4.14          (cterm_of thy elimrule')))
    4.15 -    val tac = (fn _ => setmp quick_and_dirty true SkipProof.cheat_tac thy)    
    4.16 +    val tac = (fn _ => setmp quick_and_dirty true (SkipProof.cheat_tac thy))    
    4.17      val eq = Goal.prove ctxt' [] [] (Logic.mk_equals ((Thm.prop_of elimrule), elimrule')) tac
    4.18      val _ = Output.tracing "Preprocessed elimination rule"
    4.19    in
    4.20 @@ -2205,54 +2206,7 @@
    4.21      forall (check_prem o dest_prem thy params o HOLogic.dest_Trueprop) prems
    4.22    end
    4.23  
    4.24 -fun expand_tuples thy intro =
    4.25 -  let
    4.26 -    fun rewrite_args [] (intro_t, names) = (intro_t, names)
    4.27 -      | rewrite_args (arg::args) (intro_t, names) = 
    4.28 -      (case HOLogic.strip_tupleT (fastype_of arg) of
    4.29 -        (Ts as _ :: _ :: _) =>
    4.30 -        let
    4.31 -          fun rewrite_arg' (Const ("Pair", _) $ _ $ t2, Type ("*", [_, T2]))
    4.32 -            (args, (intro_t, names)) = rewrite_arg' (t2, T2) (args, (intro_t, names))
    4.33 -            | rewrite_arg' (t, Type ("*", [T1, T2])) (args, (intro_t, names)) =
    4.34 -              let
    4.35 -                val [x, y] = Name.variant_list names ["x", "y"]
    4.36 -                val pat = (t, HOLogic.mk_prod (Free (x, T1), Free (y, T2)))
    4.37 -                val _ = tracing ("Rewriting term " ^
    4.38 -                    (Syntax.string_of_term_global thy (fst pat)) ^ " to " ^
    4.39 -                    (Syntax.string_of_term_global thy (snd pat)) ^ " in " ^
    4.40 -                  (Syntax.string_of_term_global thy intro_t))
    4.41 -                val intro_t' = Pattern.rewrite_term thy [pat] [] intro_t
    4.42 -                val args' = map (Pattern.rewrite_term thy [pat] []) args
    4.43 -              in
    4.44 -                rewrite_arg' (Free (y, T2), T2) (args', (intro_t', x::y::names))
    4.45 -              end
    4.46 -            | rewrite_arg' _ (args, (intro_t, names)) = (args, (intro_t, names))
    4.47 -          val (args', (intro_t', names')) = rewrite_arg' (arg, fastype_of arg)
    4.48 -            (args, (intro_t, names))
    4.49 -        in
    4.50 -          rewrite_args args' (intro_t', names')
    4.51 -        end
    4.52 -      | _ => rewrite_args args (intro_t, names))
    4.53 -    fun rewrite_prem (Prem (args, _)) = rewrite_args args
    4.54 -      | rewrite_prem (Negprem (args, _)) = rewrite_args args
    4.55 -      | rewrite_prem _ = I
    4.56 -    val intro_t = Logic.unvarify (prop_of intro)
    4.57 -    val frees = Term.add_free_names intro_t []
    4.58 -    val concl = Logic.strip_imp_concl intro_t
    4.59 -    val (p, args) = strip_comb (HOLogic.dest_Trueprop concl)
    4.60 -    val params = List.take (args, nparams_of thy (fst (dest_Const p)))
    4.61 -    val (intro_t', frees') = rewrite_args args (intro_t, frees)
    4.62 -    val (intro_t', _) = 
    4.63 -      fold (rewrite_prem o dest_prem thy params o HOLogic.dest_Trueprop)
    4.64 -      (Logic.strip_imp_prems intro_t') (intro_t', frees')
    4.65 -    val _ = tracing ("intro_t': " ^ (Syntax.string_of_term_global thy intro_t'))
    4.66 -    val tac = 
    4.67 -      (fn _ => setmp quick_and_dirty true SkipProof.cheat_tac thy)
    4.68 -  in
    4.69 -    Goal.prove (ProofContext.init thy) (Term.add_free_names intro_t' []) []
    4.70 -      intro_t' tac
    4.71 -  end
    4.72 +
    4.73  
    4.74  (** main function of predicate compiler **)
    4.75  
    4.76 @@ -2260,10 +2214,9 @@
    4.77    let
    4.78      val _ = Output.tracing ("Starting predicate compiler for predicates " ^ commas prednames ^ "...")
    4.79      val _ = Output.tracing (commas (map (Display.string_of_thm_global thy) (maps (intros_of thy) prednames)))
    4.80 -    val intros' = map (expand_tuples thy) (maps (intros_of thy) prednames)
    4.81 -    val _ = map (check_format_of_intro_rule thy) intros'
    4.82 +    val _ = map (check_format_of_intro_rule thy) (maps (intros_of thy) prednames)
    4.83      val (preds, nparams, all_vs, param_vs, extra_modes, clauses, all_modes) =
    4.84 -      prepare_intrs thy prednames intros'
    4.85 +      prepare_intrs thy prednames (maps (intros_of thy) prednames)
    4.86      val _ = Output.tracing "Infering modes..."
    4.87      val moded_clauses = #infer_modes steps thy extra_modes all_modes param_vs clauses 
    4.88      val modes = map (fn (p, mps) => (p, map fst mps)) moded_clauses
     5.1 --- a/src/HOL/ex/Predicate_Compile.thy	Sat Oct 24 16:55:42 2009 +0200
     5.2 +++ b/src/HOL/ex/Predicate_Compile.thy	Sat Oct 24 16:55:42 2009 +0200
     5.3 @@ -25,7 +25,7 @@
     5.4    "set xs x ==> set (x' # xs) x" 
     5.5  unfolding mem_def[symmetric, of _ x]
     5.6  by auto
     5.7 -
     5.8 +(*
     5.9  code_pred set
    5.10  proof -
    5.11    case set
    5.12 @@ -38,6 +38,7 @@
    5.13      apply auto
    5.14      done
    5.15  qed
    5.16 +*)
    5.17  
    5.18  section {* Alternative rules for list_all2 *}
    5.19  
    5.20 @@ -47,6 +48,7 @@
    5.21  lemma list_all2_ConsI [code_pred_intros]: "list_all2 P xs ys ==> P x y ==> list_all2 P (x#xs) (y#ys)"
    5.22  by auto
    5.23  
    5.24 +(*
    5.25  code_pred list_all2
    5.26  proof -
    5.27    case list_all2
    5.28 @@ -59,5 +61,5 @@
    5.29      apply auto
    5.30      done
    5.31  qed
    5.32 -
    5.33 +*)
    5.34  end
    5.35 \ No newline at end of file
     6.1 --- a/src/HOL/ex/Predicate_Compile_ex.thy	Sat Oct 24 16:55:42 2009 +0200
     6.2 +++ b/src/HOL/ex/Predicate_Compile_ex.thy	Sat Oct 24 16:55:42 2009 +0200
     6.3 @@ -55,7 +55,7 @@
     6.4  | "[| ys = fst (xa, y); x # zs = snd (xa, y);
     6.5   tupled_append' (xs, ys, x # zs) |] ==> tupled_append' (x # xs, xa, y)"
     6.6  
     6.7 -code_pred tupled_append' .
     6.8 +code_pred (inductify_all) tupled_append' .
     6.9  thm tupled_append'.equation
    6.10  (* TODO: Missing a few modes! *)
    6.11  
    6.12 @@ -64,7 +64,9 @@
    6.13    "tupled_append'' ([], xs, xs)"
    6.14  | "ys = fst yszs ==> x # zs = snd yszs ==> tupled_append'' (xs, ys, x # zs) \<Longrightarrow> tupled_append'' (x # xs, yszs)"
    6.15  
    6.16 -code_pred tupled_append'' .
    6.17 +thm tupled_append''.cases
    6.18 +
    6.19 +code_pred (inductify_all) tupled_append'' .
    6.20  thm tupled_append''.equation
    6.21  (* TODO: Missing a few modes *)
    6.22  
    6.23 @@ -73,10 +75,19 @@
    6.24    "tupled_append''' ([], xs, xs)"
    6.25  | "yszs = (ys, zs) ==> tupled_append''' (xs, yszs) \<Longrightarrow> tupled_append''' (x # xs, ys, x # zs)"
    6.26  
    6.27 -code_pred tupled_append''' .
    6.28 +code_pred (inductify_all) tupled_append''' .
    6.29  thm tupled_append'''.equation
    6.30  (* TODO: Missing a few modes *)
    6.31 +thm fst_conv snd_conv
    6.32 +thm map_of.simps
    6.33 +term "map_of"
    6.34 +inductive map_ofP :: "('a \<times> 'b) list \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool"
    6.35 +where
    6.36 +  "map_ofP ((a, b)#xs) a b"
    6.37 +| "map_ofP xs a b \<Longrightarrow> map_ofP (x#xs) a b"
    6.38  
    6.39 +code_pred map_ofP .
    6.40 +thm map_ofP.equation
    6.41  section {* reverse *}
    6.42  
    6.43  inductive rev where
    6.44 @@ -420,13 +431,13 @@
    6.45    "length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] ==> test w"
    6.46  ML {* @{term "[x \<leftarrow> w. x = a]"} *}
    6.47  code_pred (inductify_all) test .
    6.48 -
    6.49 +(*
    6.50  theorem S\<^isub>3_complete:
    6.51  "length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] \<longrightarrow> w \<in> S\<^isub>3"
    6.52  (*quickcheck[generator=SML]*)
    6.53  quickcheck[generator=pred_compile, size=10, iterations=100]
    6.54  oops
    6.55 -
    6.56 +*)
    6.57  inductive_set S\<^isub>4 and A\<^isub>4 and B\<^isub>4 where
    6.58    "[] \<in> S\<^isub>4"
    6.59  | "w \<in> A\<^isub>4 \<Longrightarrow> b # w \<in> S\<^isub>4"