added context free grammar example; removed dead code; adapted to work without quick and dirty mode; fixed typo
authorbulwahn
Wed Sep 23 16:20:12 2009 +0200 (2009-09-23)
changeset 32669462b1dd67a58
parent 32668 b2de45007537
child 32670 cc0bae788b7e
added context free grammar example; removed dead code; adapted to work without quick and dirty mode; fixed typo
src/HOL/Tools/Predicate_Compile/pred_compile_data.ML
src/HOL/Tools/Predicate_Compile/pred_compile_pred.ML
src/HOL/Tools/Predicate_Compile/predicate_compile.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
src/HOL/ex/Predicate_Compile_ex.thy
     1.1 --- a/src/HOL/Tools/Predicate_Compile/pred_compile_data.ML	Wed Sep 23 16:20:12 2009 +0200
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/pred_compile_data.ML	Wed Sep 23 16:20:12 2009 +0200
     1.3 @@ -108,7 +108,7 @@
     1.4        in ((Free (x, T), HOLogic.mk_ptuple paths T (map Free xTs)), nctxt') end
     1.5      val (rewr, _) = fold_map mk_tuple_rewrites frees nctxt 
     1.6      val t' = Pattern.rewrite_term thy rewr [] t
     1.7 -    val tac = SkipProof.cheat_tac thy
     1.8 +    val tac = setmp quick_and_dirty true (SkipProof.cheat_tac thy)
     1.9      val th'' = Goal.prove ctxt (Term.add_free_names t' []) [] t' (fn {...} => tac)
    1.10      val th''' = LocalDefs.unfold ctxt [@{thm split_conv}] th''
    1.11    in
     2.1 --- a/src/HOL/Tools/Predicate_Compile/pred_compile_pred.ML	Wed Sep 23 16:20:12 2009 +0200
     2.2 +++ b/src/HOL/Tools/Predicate_Compile/pred_compile_pred.ML	Wed Sep 23 16:20:12 2009 +0200
     2.3 @@ -56,7 +56,7 @@
     2.4      val ((_, intros), ctxt') = Variable.import true intros ctxt
     2.5      val (intros', (local_defs, thy')) = (fold_map o fold_map_atoms)
     2.6        (flatten constname) (map prop_of intros) ([], thy)
     2.7 -    val tac = fn {...} => SkipProof.cheat_tac thy'
     2.8 +    val tac = fn {...} => setmp quick_and_dirty true (SkipProof.cheat_tac thy')
     2.9      val intros'' = map (fn t => Goal.prove ctxt' [] [] t tac) intros'
    2.10        |> Variable.export ctxt' ctxt
    2.11    in
     3.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Wed Sep 23 16:20:12 2009 +0200
     3.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Wed Sep 23 16:20:12 2009 +0200
     3.3 @@ -36,7 +36,7 @@
     3.4      val _ = tracing ("intross: " ^ commas (map (Display.string_of_thm_global thy'') (flat intross)))
     3.5      val _ = priority "Replacing functions in introrules..."
     3.6      val intross' = burrow (maps (Predicate_Compile_Fun.rewrite_intro thy'')) intross
     3.7 -    val intross'' = burrow (maps remove_pointless_clauses) intross
     3.8 +    val intross'' = burrow (maps remove_pointless_clauses) intross'
     3.9      val thy''' = fold Predicate_Compile_Core.register_intros intross'' thy''
    3.10    in
    3.11      thy'''
     4.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed Sep 23 16:20:12 2009 +0200
     4.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed Sep 23 16:20:12 2009 +0200
     4.3 @@ -1623,24 +1623,11 @@
     4.4  							 val xout = Free (name_out, HOLogic.mk_tupleT Touts)
     4.5  							 val xarg = mk_arg xin xout pis T
     4.6  						 in (((if null Tins then [] else [xin], if null Touts then [] else [xout]), xarg), name_in :: name_out :: names) end
     4.7 -						(* HOLogic.strip_tupleT T of
     4.8 -						[] => 
     4.9 -							in (Free (vname, T), vname :: names) end
    4.10 -					| [_] => let val vname = Name.variant names ("x" ^ string_of_int (length Ts1' + i))
    4.11 -							in (Free (vname, T), vname :: names) end
    4.12 -					| Ts =>
    4.13 -						let
    4.14 -							val vnames = Name.variant_list names
    4.15 -								(map (fn j => "x" ^ string_of_int (length Ts1' + i) ^ "p" ^ string_of_int j)
    4.16 -									(1 upto (length Ts)))
    4.17 -						 in (HOLogic.mk_tuple (map Free (vnames ~~ Ts)), vnames @ names) end *)
    4.18 -				end
    4.19 +						 end
    4.20     	  val (xinoutargs, names) = fold_map mk_vars ((1 upto (length Ts2)) ~~ Ts2) param_names
    4.21        val (xinout, xargs) = split_list xinoutargs
    4.22  			val (xins, xouts) = pairself flat (split_list xinout)
    4.23 -			(*val (xins, xouts) = split_smode is xargs*)
    4.24  			val (xparams', names') = fold_map mk_Eval_of ((xparams ~~ Ts1) ~~ iss) names
    4.25 -			val _ = Output.tracing ("xargs:" ^ commas (map (Syntax.string_of_term_global thy) xargs))
    4.26        fun mk_split_lambda [] t = lambda (Free (Name.variant names' "x", HOLogic.unitT)) t
    4.27          | mk_split_lambda [x] t = lambda x t
    4.28          | mk_split_lambda xs t =
    4.29 @@ -2107,7 +2094,7 @@
    4.30      (join_preds_modes moded_clauses compiled_terms)
    4.31  
    4.32  fun prove_by_skip thy _ _ _ _ compiled_terms =
    4.33 -  map_preds_modes (fn pred => fn mode => fn t => Drule.standard (SkipProof.make_thm thy t))
    4.34 +  map_preds_modes (fn pred => fn mode => fn t => Drule.standard (setmp quick_and_dirty true (SkipProof.make_thm thy) t))
    4.35      compiled_terms
    4.36      
    4.37  fun prepare_intrs thy prednames =
     5.1 --- a/src/HOL/ex/Predicate_Compile_ex.thy	Wed Sep 23 16:20:12 2009 +0200
     5.2 +++ b/src/HOL/ex/Predicate_Compile_ex.thy	Wed Sep 23 16:20:12 2009 +0200
     5.3 @@ -252,4 +252,26 @@
     5.4  thm Domain.equation
     5.5  
     5.6  
     5.7 +section {* Context Free Grammar *}
     5.8 +
     5.9 +datatype alphabet = a | b
    5.10 +
    5.11 +inductive_set S\<^isub>1 and A\<^isub>1 and B\<^isub>1 where
    5.12 +  "[] \<in> S\<^isub>1"
    5.13 +| "w \<in> A\<^isub>1 \<Longrightarrow> b # w \<in> S\<^isub>1"
    5.14 +| "w \<in> B\<^isub>1 \<Longrightarrow> a # w \<in> S\<^isub>1"
    5.15 +| "w \<in> S\<^isub>1 \<Longrightarrow> a # w \<in> A\<^isub>1"
    5.16 +| "w \<in> S\<^isub>1 \<Longrightarrow> b # w \<in> S\<^isub>1"
    5.17 +| "\<lbrakk>v \<in> B\<^isub>1; v \<in> B\<^isub>1\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>1"
    5.18 +
    5.19 +code_pred (inductify_all) S\<^isub>1p .
    5.20 +
    5.21 +thm S\<^isub>1p.equation
    5.22 +
    5.23 +code_pred (inductify_all) (rpred) S\<^isub>1p .
    5.24 +
    5.25 +thm S\<^isub>1p.rpred_equation
    5.26 +
    5.27 +
    5.28 +
    5.29  end
    5.30 \ No newline at end of file