src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy
changeset 39919 9f6503aaa77d
parent 39302 d7728f65b353
child 40054 cd7b1fa20bce
     1.1 --- a/src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy	Mon Oct 04 14:46:49 2010 +0200
     1.2 +++ b/src/HOL/Predicate_Compile_Examples/Specialisation_Examples.thy	Mon Oct 04 14:46:49 2010 +0200
     1.3 @@ -4,7 +4,7 @@
     1.4  
     1.5  section {* Specialisation Examples *}
     1.6  
     1.7 -fun nth_el'
     1.8 +primrec nth_el'
     1.9  where
    1.10    "nth_el' [] i = None"
    1.11  | "nth_el' (x # xs) i = (case i of 0 => Some x | Suc j => nth_el' xs j)"
    1.12 @@ -48,7 +48,27 @@
    1.13  
    1.14  subsection {* Sorts *}
    1.15  
    1.16 -code_pred [inductify] sorted .
    1.17 +declare sorted.Nil [code_pred_intro]
    1.18 +  sorted_single [code_pred_intro]
    1.19 +  sorted_many [code_pred_intro]
    1.20 +
    1.21 +code_pred sorted proof -
    1.22 +  assume "sorted xa"
    1.23 +  assume 1: "xa = [] \<Longrightarrow> thesis"
    1.24 +  assume 2: "\<And>x. xa = [x] \<Longrightarrow> thesis"
    1.25 +  assume 3: "\<And>x y zs. xa = x # y # zs \<Longrightarrow> x \<le> y \<Longrightarrow> sorted (y # zs) \<Longrightarrow> thesis"
    1.26 +  show thesis proof (cases xa)
    1.27 +    case Nil with 1 show ?thesis .
    1.28 +  next
    1.29 +    case (Cons x xs) show ?thesis proof (cases xs)
    1.30 +      case Nil with Cons 2 show ?thesis by simp
    1.31 +    next
    1.32 +      case (Cons y zs) with `xa = x # xs` have "xa = x # y # zs" by simp
    1.33 +      moreover with `sorted xa` have "x \<le> y" and "sorted (y # zs)" by simp_all
    1.34 +      ultimately show ?thesis by (rule 3)
    1.35 +    qed
    1.36 +  qed
    1.37 +qed
    1.38  thm sorted.equation
    1.39  
    1.40  section {* Specialisation in POPLmark theory *}
    1.41 @@ -212,10 +232,10 @@
    1.42  where
    1.43    T_Var: "\<Gamma> \<turnstile>\<^bsub>wf\<^esub> \<Longrightarrow> \<Gamma>\<langle>i\<rangle> = \<lfloor>VarB U\<rfloor> \<Longrightarrow> T = \<up>\<^isub>\<tau> (Suc i) 0 U \<Longrightarrow> \<Gamma> \<turnstile> Var i : T"
    1.44  | T_Abs: "VarB T\<^isub>1 \<Colon> \<Gamma> \<turnstile> t\<^isub>2 : T\<^isub>2 \<Longrightarrow> \<Gamma> \<turnstile> (\<lambda>:T\<^isub>1. t\<^isub>2) : T\<^isub>1 \<rightarrow> \<down>\<^isub>\<tau> 1 0 T\<^isub>2"
    1.45 -| T_App: "\<Gamma> \<turnstile> t\<^isub>1 : T\<^isub>1\<^isub>1 \<rightarrow> T\<^isub>1\<^isub>2 \<Longrightarrow> \<Gamma> \<turnstile> t\<^isub>2 : T\<^isub>1\<^isub>1 \<Longrightarrow> \<Gamma> \<turnstile> t\<^isub>1 \<bullet> t\<^isub>2 : T\<^isub>1\<^isub>2"
    1.46 +| T_App: "\<Gamma> \<turnstile> t\<^isub>1 : T\<^isub>11 \<rightarrow> T\<^isub>12 \<Longrightarrow> \<Gamma> \<turnstile> t\<^isub>2 : T\<^isub>11 \<Longrightarrow> \<Gamma> \<turnstile> t\<^isub>1 \<bullet> t\<^isub>2 : T\<^isub>12"
    1.47  | T_TAbs: "TVarB T\<^isub>1 \<Colon> \<Gamma> \<turnstile> t\<^isub>2 : T\<^isub>2 \<Longrightarrow> \<Gamma> \<turnstile> (\<lambda><:T\<^isub>1. t\<^isub>2) : (\<forall><:T\<^isub>1. T\<^isub>2)"
    1.48 -| T_TApp: "\<Gamma> \<turnstile> t\<^isub>1 : (\<forall><:T\<^isub>1\<^isub>1. T\<^isub>1\<^isub>2) \<Longrightarrow> \<Gamma> \<turnstile> T\<^isub>2 <: T\<^isub>1\<^isub>1 \<Longrightarrow>
    1.49 -    \<Gamma> \<turnstile> t\<^isub>1 \<bullet>\<^isub>\<tau> T\<^isub>2 : T\<^isub>1\<^isub>2[0 \<mapsto>\<^isub>\<tau> T\<^isub>2]\<^isub>\<tau>"
    1.50 +| T_TApp: "\<Gamma> \<turnstile> t\<^isub>1 : (\<forall><:T\<^isub>11. T\<^isub>12) \<Longrightarrow> \<Gamma> \<turnstile> T\<^isub>2 <: T\<^isub>11 \<Longrightarrow>
    1.51 +    \<Gamma> \<turnstile> t\<^isub>1 \<bullet>\<^isub>\<tau> T\<^isub>2 : T\<^isub>12[0 \<mapsto>\<^isub>\<tau> T\<^isub>2]\<^isub>\<tau>"
    1.52  | T_Sub: "\<Gamma> \<turnstile> t : S \<Longrightarrow> \<Gamma> \<turnstile> S <: T \<Longrightarrow> \<Gamma> \<turnstile> t : T"
    1.53  
    1.54  code_pred [inductify, skip_proof, specialise] typing .