compile
authorblanchet
Wed Feb 12 08:37:28 2014 +0100 (2014-02-12)
changeset 554226445a05a1234
parent 55421 0aaca907aeab
child 55423 07dea66779f3
compile
src/Doc/Codegen/Refinement.thy
src/HOL/Decision_Procs/Cooper.thy
src/HOL/Decision_Procs/Ferrack.thy
src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
     1.1 --- a/src/Doc/Codegen/Refinement.thy	Wed Feb 12 08:37:28 2014 +0100
     1.2 +++ b/src/Doc/Codegen/Refinement.thy	Wed Feb 12 08:37:28 2014 +0100
     1.3 @@ -148,15 +148,15 @@
     1.4    \noindent It is good style, although no absolute requirement, to
     1.5    provide code equations for the original artefacts of the implemented
     1.6    type, if possible; in our case, these are the datatype constructor
     1.7 -  @{const Queue} and the case combinator @{const queue_case}:
     1.8 +  @{const Queue} and the case combinator @{const case_queue}:
     1.9  *}
    1.10  
    1.11  lemma %quote Queue_AQueue [code]:
    1.12    "Queue = AQueue []"
    1.13    by (simp add: AQueue_def fun_eq_iff)
    1.14  
    1.15 -lemma %quote queue_case_AQueue [code]:
    1.16 -  "queue_case f (AQueue xs ys) = f (ys @ rev xs)"
    1.17 +lemma %quote case_queue_AQueue [code]:
    1.18 +  "case_queue f (AQueue xs ys) = f (ys @ rev xs)"
    1.19    by (simp add: AQueue_def)
    1.20  
    1.21  text {*
    1.22 @@ -164,7 +164,7 @@
    1.23  *}
    1.24  
    1.25  text %quotetypewriter {*
    1.26 -  @{code_stmts empty enqueue dequeue Queue queue_case (SML)}
    1.27 +  @{code_stmts empty enqueue dequeue Queue case_queue (SML)}
    1.28  *}
    1.29  
    1.30  text {*
    1.31 @@ -274,4 +274,3 @@
    1.32  *}
    1.33  
    1.34  end
    1.35 -
     2.1 --- a/src/HOL/Decision_Procs/Cooper.thy	Wed Feb 12 08:37:28 2014 +0100
     2.2 +++ b/src/HOL/Decision_Procs/Cooper.thy	Wed Feb 12 08:37:28 2014 +0100
     2.3 @@ -303,12 +303,12 @@
     2.4  lemma evaldjf_bound0:
     2.5    assumes nb: "\<forall>x\<in> set xs. bound0 (f x)"
     2.6    shows "bound0 (evaldjf f xs)"
     2.7 -  using nb by (induct xs) (auto simp add: evaldjf_def djf_def Let_def, case_tac "f x1", auto)
     2.8 +  using nb by (induct xs) (auto simp add: evaldjf_def djf_def Let_def, case_tac "f a", auto)
     2.9  
    2.10  lemma evaldjf_qf:
    2.11    assumes nb: "\<forall>x\<in> set xs. qfree (f x)"
    2.12    shows "qfree (evaldjf f xs)"
    2.13 -  using nb by (induct xs) (auto simp add: evaldjf_def djf_def Let_def, case_tac "f x1", auto)
    2.14 +  using nb by (induct xs) (auto simp add: evaldjf_def djf_def Let_def, case_tac "f a", auto)
    2.15  
    2.16  fun disjuncts :: "fm \<Rightarrow> fm list"
    2.17  where
     3.1 --- a/src/HOL/Decision_Procs/Ferrack.thy	Wed Feb 12 08:37:28 2014 +0100
     3.2 +++ b/src/HOL/Decision_Procs/Ferrack.thy	Wed Feb 12 08:37:28 2014 +0100
     3.3 @@ -328,12 +328,12 @@
     3.4  lemma evaldjf_bound0: 
     3.5    assumes nb: "\<forall> x\<in> set xs. bound0 (f x)"
     3.6    shows "bound0 (evaldjf f xs)"
     3.7 -  using nb by (induct xs, auto simp add: evaldjf_def djf_def Let_def) (case_tac "f x1", auto) 
     3.8 +  using nb by (induct xs, auto simp add: evaldjf_def djf_def Let_def) (case_tac "f a", auto) 
     3.9  
    3.10  lemma evaldjf_qf: 
    3.11    assumes nb: "\<forall> x\<in> set xs. qfree (f x)"
    3.12    shows "qfree (evaldjf f xs)"
    3.13 -  using nb by (induct xs, auto simp add: evaldjf_def djf_def Let_def) (case_tac "f x1", auto) 
    3.14 +  using nb by (induct xs, auto simp add: evaldjf_def djf_def Let_def) (case_tac "f a", auto) 
    3.15  
    3.16  fun disjuncts :: "fm \<Rightarrow> fm list" where
    3.17    "disjuncts (Or p q) = disjuncts p @ disjuncts q"
    3.18 @@ -2030,4 +2030,3 @@
    3.19    by rferrack
    3.20  
    3.21  end
    3.22 -
     4.1 --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Wed Feb 12 08:37:28 2014 +0100
     4.2 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Wed Feb 12 08:37:28 2014 +0100
     4.3 @@ -761,12 +761,12 @@
     4.4  lemma evaldjf_bound0: 
     4.5    assumes nb: "\<forall> x\<in> set xs. bound0 (f x)"
     4.6    shows "bound0 (evaldjf f xs)"
     4.7 -  using nb by (induct xs, auto simp add: evaldjf_def djf_def Let_def) (case_tac "f x1", auto) 
     4.8 +  using nb by (induct xs, auto simp add: evaldjf_def djf_def Let_def) (case_tac "f a", auto) 
     4.9  
    4.10  lemma evaldjf_qf: 
    4.11    assumes nb: "\<forall> x\<in> set xs. qfree (f x)"
    4.12    shows "qfree (evaldjf f xs)"
    4.13 -  using nb by (induct xs, auto simp add: evaldjf_def djf_def Let_def) (case_tac "f x1", auto) 
    4.14 +  using nb by (induct xs, auto simp add: evaldjf_def djf_def Let_def) (case_tac "f a", auto) 
    4.15  
    4.16  fun disjuncts :: "fm \<Rightarrow> fm list" where
    4.17    "disjuncts (Or p q) = (disjuncts p) @ (disjuncts q)"