# Theory Intensional

theory Intensional
imports Main

section

theory Intensional
imports Main
begin

class world

type_synonym ('w,'a) expr =
type_synonym 'w form =

definition Valid ::
where

definition const ::
where unl_con:

definition lift ::
where unl_lift:

definition lift2 ::
where unl_lift2:

definition lift3 ::
where unl_lift3:

definition RAll ::   (binder  10)
where unl_Rall:
definition REx ::   (binder  10)
where unl_Rex:
definition REx1 ::   (binder  10)
where unl_Rex1:

nonterminal lift and liftargs

syntax
::                           ()
::                       ()
::                          ()
::                ( [1000, 1000] 999)
::                         ()
::                   ( [0, 3] 3)
::                 ( [4, 0] 3)
::                     ()
::         ()
::                         ( 5)
::                   ( [100,10] 10)

::                           ()

::                           ( [1000] 999)
::                   ( [1000] 999)
::             ( [1000] 999)
::       ( [1000] 999)

::                 ( [50,51] 50)
::                 ( [50,51] 50)
::                         ( [40] 40)
::                 ( [36,35] 35)
::                 ( [31,30] 30)
::                 ( [26,25] 25)
::           ( 10)
::                 ( [66,65] 65)
::                 ( [66,65] 65)
::                 ( [71,70] 70)
::                 ( [71,70] 70)
::                 ( [71,70] 70)
::                 (  [50, 51] 50)
::                 ( [50, 51] 50)
::                 ( [50, 51] 50)
::                 ( [50, 51] 50)
::                     ()

::                    ()

::                   ( [65,66] 65)
::                   ( [65,66] 65)
::                       ()

::                       ( [0, 10] 10)
::                       ( [0, 10] 10)
::                       ( [0, 10] 10)

translations
==
==
==
==
==
==
==
==

=>
=>

==
==
==
==
==
==
==
==
==
==
==
==
==
==
==
==
==
==
==
==
==
==
==
==

<=
<=
<=
<=
<=
<=
<=
<=

subsection

lemmas intensional_rews [simp] =
unl_con unl_lift unl_lift2 unl_lift3 unl_Rall unl_Rex unl_Rex1

lemma inteq_reflection:
apply (unfold Valid_def unl_lift2)
apply (rule eq_reflection)
apply (rule ext)
apply (erule spec)
done

lemma intI [intro!]:
apply (unfold Valid_def)
apply (rule allI)
apply (erule meta_spec)
done

lemma intD [dest]:
apply (unfold Valid_def)
apply (erule spec)
done

lemma int_simps:

apply (unfold Valid_def intensional_rews)
apply blast+
done

declare int_simps [THEN inteq_reflection, simp]

lemma TrueW [simp]:

ML

attribute_setup int_unlift =

attribute_setup int_rewrite =

attribute_setup flatten =

attribute_setup int_use =

lemma Not_Rall: